--- layout: fc_discuss_archives title: Message 127 from Frama-C-discuss on October 2008 ---
Hi, I tried the last version released (Lithium) on your struct example, it works properly and all VC are proved with any of Alt-Ergo, Simplify or Z3 prover (but not Yices). On your enum examples, I got an error in function p1: Error: Casting from type int to type struct enum___anonenum_RESULTAT_1_P * not allowed This is because you assign [last] instead of [*last]. Then, for the case without function, I had to rewrite function [function2_res] to add an obvious cast to [RESULTAT] /*@ predicate function2_res{L}(int n) = @ result((RESULTAT)OK,n); @*/ This is a bug (no cast should be needed here), for which I have filled bug 6622 in the public BTS of Frama-C. Except that, some VC are not proved because not provable. On your last enum example with function, the verification proceeds adequately. Of course, some VC are not proved because not provable. HTH, -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081031/94052e85/attachment.htm