--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on January 2011 ---
Hi all, I tried to prove my program without the struct and it succeeded !!! Maybe I have to create some logic specification for the struct ? Or something to help the solver to understand what is on the structure. You could find enclosed the new c-code. I will now try to add some "structure specification". -------------- next part -------------- A non-text attachment was scrubbed... Name: sum_list.c Type: application/octet-stream Size: 1117 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110125/09ba5985/attachment.obj> -------------- next part -------------- Arnaud On Jan 24, 2011, at 9:05 PM, David MENTRE wrote: > Hello, > > 2011/1/24 David MENTRE <dmentre at linux-france.org>: >> Yes. Please find attached a variation of Arnaud's program that >> compiles and runs under Jessie. >> >> I really don't understand why the assert in the for() loop of function >> f() (VC 6.) is not proved. >> >> I'm using Frama-C Boron with Alt-Ergo 0.91. > > I still cannot prove the assertion with Frama-C Carbon beta 2, Why > 2.28 and Alt-ergo 0.91[1]. The problem is probably in the assertion > itself, but I don't see where. > > Regards, > d. > > [1] And a slight modification on annotations, see attached C file. > <dieumegard-case2.c>_______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss Cordialement, Arnaud Dieumegard Research engineer IRIT / ACADIE arnaud.dieumegard at enseeiht.fr