2021-01-26 19:18 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000329Frama-CKernel > ACSL implementationpublic2014-02-12 16:55
Reportersboldo 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000329: Float promoted to double
DescriptionI am in the svn 33841 version.

In the given file, the float x is propoted by frama-c to a double precision number by frama-c itself (frama-c-gui):
instead of \exact(x)
I have \exact((double )x)
TagsNo tags attached.
Attached Files
  • c file icon machin.c (324 bytes) 2009-11-13 13:58 -
    #pragma JessieFloatModel(strict)
    
    /*@ requires \abs(\exact(x)) <= 0x1p-5 
      @     && \round_error(x) <= 0x1p-20;  
      @ ensures \abs(\exact(\result) - \cos(\exact(x))) <= 0x1p-24
      @     && \round_error(\result) <= \round_error(x) + 0x3p-24;  
      @*/
    float cosine1a(float x) {
      float r = 1.0f - x * x * 0.5f;
      return r;
    }
    
    
    c file icon machin.c (324 bytes) 2009-11-13 13:58 +

-Relationships
+Relationships

-Notes

~0000559

virgile (developer)

- At the moment, there's only one exact built-in in the logic, which takes double as argument.
- I suspect that overloading resolution is not equipped to deal with a float and a double version.

~0000560

cmarche (developer)

- Good guess: the \exact built-in for float is comment out !
- Bad guess: overloading deals with float and double, e.g with \sign

I guess that uncommmenting the \exact(float) will magically fix the bug...

~0000561

cmarche (developer)

Fixed in cil/src/logic_builtins.ml, uncommented definitions for floats parameters.
+Notes

-Issue History
Date Modified Username Field Change
2009-11-13 13:58 sboldo New Issue
2009-11-13 13:58 sboldo File Added: machin.c
2009-11-13 16:30 signoles Status new => assigned
2009-11-13 16:30 signoles Assigned To => virgile
2009-11-13 16:40 virgile Note Added: 0000559
2009-11-13 16:40 virgile Assigned To virgile => cmarche
2009-11-13 16:58 cmarche Note Added: 0000560
2009-11-13 17:03 cmarche Note Added: 0000561
2009-11-13 17:03 cmarche Status assigned => resolved
2009-11-13 17:03 cmarche Resolution open => fixed
2009-11-13 17:04 svn
2010-02-05 09:46 signoles Category Kernel => Kernel > ACSL implementation
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron
2013-12-19 01:13 cmarche Source_changeset_attached => framac master 7d796f3d
2014-02-12 16:55 cmarche Source_changeset_attached => framac stable/neon 7d796f3d
+Issue History