--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2011 ---
On Wednesday, July 13, 2011, mars Gu <marsishandsome at gmail.com> wrote: > i find a problem with the wp plugin in?Frama-C, whose version is "Frama-C > Carbon-20110201+dev". > 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 ... Regardless of the details of the case, I must reiterate that the pattern above is almost never the pattern of an interesting bug report. Automatic provers prove some true properties, and hopefully never any false properties. There are countless true and non-alt-ergo-provable properties. Among these, there are countless that would be provable if they were just a little bit simpler. You will encounter them. Please do not think you have found a problem each time you find one of them.