Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Filesc file icon machin.c [^] (324 bytes) 2009-11-13 13:58 [Show Content]

- Relationships

-  Notes
(0000559)
virgile (developer)
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 (developer)
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 (developer)
2009-11-13 17:03

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

- 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 Checkin
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker