--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on June 2011 ---
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>