--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on September 2013 ---
Hello, In the attached find.c example, everything is proved with WP (loop invariant, function contract). However, if I remove the "loop assigns i;" in the for loop, the ensures clauses of the function contract are not proved any more. Can somebody explain to me why, as I think my loop invariant is building all the information needed to prove the ensures clauses. As far as I remember, this was not the case with previous version of Frama-C (or with Jessie?). Best regards, david -------------- next part -------------- A non-text attachment was scrubbed... Name: find.c Type: text/x-csrc Size: 540 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130909/6d13e707/attachment.c>