--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2011 ---
I did not try it yet, but I guess it is the same problem about labels that I pointed out in your previous example. Thanks again for your report. L. Le 5 ao?t 11 ? 12:16, mars Gu a ?crit : > 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 > < > max_element1 > .c><max_element2.c>_______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/4a3ea19c/attachment.htm>