--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp loop invariant problem



Hi,

i find a bug with the wp plugin in Frama-C, whose version is "Frama-C
Carbon-20110201+dev".
I start Frama-C with the following command:  "frama-c-gui -wp  -wp-proof
alt-ergo max_element1.c &".

In the file "max_element1.c", Frama-C can prove all the specifications.

But in the file "max_element2.c", in Line 47,
I replace "loop invariant !(\exists integer k; 0 <= k < i && (a[max] <
a[k]));"
with "loop invariant IsMaximum(a, i, max);" which are the same.
But in this case, Frama-C can not prove.


And also in the file "max_element3.c",
Line 55 can be proved while Line 44 can not.
The only difference between Line55 and Line44 is, that
Line 44 is a loop invariant, while Line 55 is an assersion.


Liangliang Gu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110629/b28d8c7c/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element1.c
Type: text/x-csrc
Size: 1426 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110629/b28d8c7c/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element2.c
Type: text/x-csrc
Size: 1426 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110629/b28d8c7c/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element3.c
Type: text/x-csrc
Size: 1424 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110629/b28d8c7c/attachment-0002.c>