--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: assigns needed to prove function contract?



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>