Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] wp <==> problem
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Wed, 13 Jul 2011 13:48:40 +0200
  • In-reply-to: <CAE6MND50AYmUrv3TZ7XSNqDTww90LEJZQ=LREZcAs3NotgHf-A@mail.gmail.com>
  • References: <CAE6MND50AYmUrv3TZ7XSNqDTww90LEJZQ=LREZcAs3NotgHf-A@mail.gmail.com>
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.