Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000367Frama-CPlug-in > jessiepublic2010-01-07 16:462010-04-19 16:14
Reportertoomanycsh 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0000617)
signoles (manager)
2010-01-08 11:00

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)
2010-01-08 13:12

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)
2010-04-19 16:14

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

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker