--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2011 ---
Hi, i really appreciate your help for the last problem about "<==>", which is already solved. But when I continue to prove, a problem occurs, which makes me confused. In the file "binary_search3.c", in line 46, "HasValue(a, n, val) <==> r;" can be proved by WP, while in line 47, " r <==> HasValue(a, n, val);" cannot. The only difference between line 46 and 47 is, that the left and the right side is exchanged. It will be better, if WP can prove this specification. My Frama-C's Version is "Frama-C Carbon-20110201+dev". I start Frama-C with the following command: "frama-c-gui -wp -wp-proof alt-ergo binary_search3.c &". Liangliang Gu -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110713/74ea0220/attachment.htm> -------------- next part -------------- A non-text attachment was scrubbed... Name: binary_search3.c Type: text/x-csrc Size: 1144 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110713/74ea0220/attachment.c>