--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp <==> problem



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.