--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Binary search now works with Alt-Ergo 0.92



Le jeu. 30 sept. 2010 09:10:00 CEST,
David MENTRE <dmentre at linux-france.org> a ?crit :

> 2010/9/28 Boris Hollas <hollas at informatik.htw-dresden.de>:
> > Alt-Ergo 0.92 is available on http://alt-ergo.lri.fr/. Now, the binary
> > search example with the faulty mid value computation
> > ? ?mid = (high + low) / 2;
> > doesn't pass verification anymore. this is good news [...]
> 
> Could you give more context? Why is it good news that an example
> doesn't pass verification anymore? I'm puzzled. :-)
> 

Because this example is not correct: high + low might overflow (see e.g.
http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html).
Thus it is better that alt-ergo does not discharge all proof
obligations in this case ;-)

-- 
E tutto per oggi, a la prossima volta.
Virgile