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] Binary search now works with Alt-Ergo 0.92

  • Subject: [Frama-c-discuss] Binary search now works with Alt-Ergo 0.92
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 30 Sep 2010 09:46:34 +0200
  • In-reply-to: <AANLkTinQpoR2tTrzEL=18tGThrKE+MfRLE6KB60XfSjL@mail.gmail.com>
  • References: <1285673055.1497.159.camel@iti27> <AANLkTinQpoR2tTrzEL=18tGThrKE+MfRLE6KB60XfSjL@mail.gmail.com>
> Could you give more context? Why is it good news that an example
> doesn't pass verification anymore? I'm puzzled. :-)

When the example has a definite bug, it is good news that it no longer
passes verification. Alt-ergo 0.91 had a bug that was apparently
linked to the presence of divisions in the target program.

See bugs:
http://bts.frama-c.com/view.php?id=539 as well as 533, 514, 571.