2021-01-18 17:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000367Frama-CPlug-in > jessiepublic2010-04-19 16:14
Reportertoomanycsh 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000367: bug with constants like 1E-6
Descriptionbool_t func1(float32_t x);
/*@ ensures \result == TRUE
  
*/
bool_t func1(float32_t x)
 {
    if (x < 1E-6){
       ;
    }
   
    return TRUE;
}

Alt-Ergo and CVC3 claim a syntax error on the input from Frama-C.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000617

signoles (manager)

From an original post on Frama-C discuss: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001745.html

The given program does not compile. Below is a proper reproducible case showing the issue with 1E-6. The outputs of Alt-Ergo and Z3 (at least) are incorrect. Ok for Simplify. I didn't test the other provers.

=== t.c ===
#define bool_t int
#define float32_t float
#define TRUE 1

bool_t func1(float32_t x);
/*@ ensures \result == TRUE;
  
*/
bool_t func1(float32_t x)
 {
    if (x < 1E-6){
       ;
    }
   
    return TRUE;
}
===========
$ frama-c -pp-annot -jessie t.c

~0000618

cmarche (developer)

fixed SMT output for Z3, Yices and CVC3

For alt-ergo, this is an alt-ergo bug, fixed in the develpment version of alt-ergo

~0000782

signoles (manager)

Fix in Why 2.24 (require Frama-C Boron-20100401).
+Notes

-Issue History
Date Modified Username Field Change
2010-01-07 16:46 toomanycsh New Issue
2010-01-08 11:00 signoles Note Added: 0000617
2010-01-08 11:00 signoles Assigned To => cmarche
2010-01-08 11:00 signoles Status new => assigned
2010-01-08 11:00 signoles Category kernel => plug-in > jessie
2010-01-08 11:00 signoles Summary bug => bug with constants like 1E-6
2010-01-08 13:12 cmarche Note Added: 0000618
2010-01-08 13:12 cmarche Status assigned => resolved
2010-01-08 13:12 cmarche Resolution open => fixed
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000782
+Issue History