Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp loop invariant problem

  • Subject: [Frama-c-discuss] wp loop invariant problem
  • From: marsishandsome at gmail.com (mars Gu)
  • Date: Wed, 29 Jun 2011 10:14:49 +0200
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>