Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000329Frama-CKernel > ACSL implementationpublic2009-11-13 13:582014-02-12 16:55
Reportersboldo 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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.
Relationships
Attached Filesc machin.c (324) 2009-11-13 13:58
https://bts.frama-c.com/file_download.php?file_id=32&type=bug

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.

Issue History
Date ModifiedUsernameFieldChange
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:04svn
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
2013-12-19 01:13cmarcheSource_changeset_attached => framac master 7d796f3d
2014-02-12 16:55cmarcheSource_changeset_attached => framac stable/neon 7d796f3d