--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on July 2011 ---
Hi, i find a problem 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 binary_search2.c &". In the file "binary_search2.c", Frama-c can prove line 46,47,49, but line 51. If line 46,46,49 can be proved, line 51 should be proved. Because if 1:a<==>b 2:b<==>c 3:(a<==>b && b<==>c) ==> (a<==>c) is true, then 4: a<==>c should also be true. Liangliang Gu -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110713/4fa31a5b/attachment.htm> -------------- next part -------------- A non-text attachment was scrubbed... Name: binary_search2.c Type: text/x-csrc Size: 1354 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110713/4fa31a5b/attachment.c>