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] bug in value analysis of programs with floating-point computations

  • Subject: [Frama-c-discuss] bug in value analysis of programs with floating-point computations
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sun, 6 Jun 2010 00:44:49 +0200
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