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
- Prev by Date: [Frama-c-discuss] Unknows Pragma
- Next by Date: [Frama-c-discuss] Combining Simplify and Coq
- Previous by thread: [Frama-c-discuss] Unknows Pragma
- Next by thread: [Frama-c-discuss] Combining Simplify and Coq
- Index(es):