--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2010 ---
The pitch: A bug has been found in the value analysis' handling of some floating-point computations (thanks to Dillon Pariente for reporting the bug). It is a correctness bug: it may cause the value analysis to declare "safe" a program that isn't. Such bugs are rare enough that I thought I would post the patch against 20100401 here for reference. The bug is present in older releases too. If you do not use the value analysis or do not analyze programs with floating-point operations, you do not have to apply this patch. The patch: Manzana:frama-c-Boron-20100401 pascal$ diff -u src/ai/ival.ml{~,} --- src/ai/ival.ml~ 2010-04-13 13:52:01.000000000 +0200 +++ src/ai/ival.ml 2010-06-05 23:52:52.000000000 +0200 @@ -482,8 +482,8 @@ then f1 else inject b1 e2 - let filter_ge (I(b1, e1) as f1) (I(b2, e2)) = - let b2 = if F.equal_ieee F.minus_zero e2 then F.minus_zero else b2 in + let filter_ge (I(b1, e1) as f1) (I(b2, _e2)) = + let b2 = if F.equal_ieee F.minus_zero b2 then F.minus_zero else b2 in if not (F.le b2 e1) then raise Bottom else if F.le b2 b1