--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on September 2010 ---
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