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] Problem with using "predicate" in "loop invariant"

  • Subject: [Frama-c-discuss] Problem with using "predicate" in "loop invariant"
  • From: marsishandsome at gmail.com (mars Gu)
  • Date: Fri, 5 Aug 2011 12:16:01 +0200
Hi,

I find a problem when using "predicate" in "loop invariant".
I use the wp plugin of 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.
In the file "max_element1.c", in Line 43,   "loop invariant !(\exists
integer k; 0 <= k < i && (a[max] <a[k]));"  can be proved, while
in the file "max_element2.c", in Line 43,   "loop invariant IsMaximum(a, i,
max);" cannot be proved.

According to the predicate "IsMaximum":
" predicate IsMaximum{L}(value_type* a, integer n, integer max) =

 10 max_element.h   | 10     !(\exists integer i; 0 <= i < n && (a[max] <
a[i]));",
the two "loop invariant"s represent the same meaning.

If Frama-c with plugin wp can prove the first "loop invariant", it should
also be able to prove the second "loop invariant".

Liangliang Gu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element1.c
Type: text/x-csrc
Size: 1174 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element2.c
Type: text/x-csrc
Size: 1143 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment-0001.c>