Frama-C Bug Tracking System - Frama-C
View Issue Details
0000329Frama-CKernel > ACSL implementationpublic2009-11-13 13:582014-02-12 16:55
sboldo 
cmarche 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Boron-20100401 
0000329: Float promoted to double
I 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)
No tags attached.
c machin.c (324) 2009-11-13 13:58
https://bts.frama-c.com/file_download.php?file_id=32&type=bug
Issue History
2009-11-13 13:58sboldoNew Issue
2009-11-13 13:58sboldoFile Added: machin.c
2009-11-13 16:30signolesStatusnew => assigned
2009-11-13 16:30signolesAssigned To => virgile
2009-11-13 16:40virgileNote Added: 0000559
2009-11-13 16:40virgileAssigned Tovirgile => cmarche
2009-11-13 16:58cmarcheNote Added: 0000560
2009-11-13 17:03cmarcheNote Added: 0000561
2009-11-13 17:03cmarcheStatusassigned => resolved
2009-11-13 17:03cmarcheResolutionopen => fixed
2009-11-13 17:04svnCheckin
2010-02-05 09:46signolesCategoryKernel => Kernel > ACSL implementation
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron

Notes
(0000559)
virgile   
2009-11-13 16:40   
- 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   
2009-11-13 16:58   
- 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   
2009-11-13 17:03   
Fixed in cil/src/logic_builtins.ml, uncommented definitions for floats parameters.