--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2011 ---
Hi, On 13/07/2011 11:50, mars Gu wrote: > 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. Your b in 1 and in 2 are not the same: please be careful with "<=" versus "<" Generally speaking, I don't think you need to use so many <==> in specifications. See for example http://proval.lri.fr/gallery/BinarySearchACSL.en.html for a correct ASL-annotated binary search function - Claude