--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on January 2011 ---
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. -------------- next part -------------- A non-text attachment was scrubbed... Name: dieumegard-case2.c Type: text/x-csrc Size: 1459 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110124/d533c2a0/attachment.c>