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

[Frama-c-discuss] bug in value analysis of programs with floating-point computations



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