Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000386Frama-CPlug-in > jessiepublic2010-02-01 09:422010-04-19 16:14
Reportersboldo 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000386: int32 and real can't be unified
DescriptionHello, With the svn version of frama-c and jessie, I have the following problem: an integer cannot be promoted to real inside a function call. The function \pow takes 2 real numbers. If I give it an int32. Jessie fails to type it.
Additional Information# pragma JessieFloatModel(strict) double malcolm1() { double A; A=2.0; /*@ assert A==2.; */ /*@ ghost int i = 1; */ /*@ loop invariant A== \pow(2.,i) && @ 1 <= i <= 53; @ loop variant (53-i); */ while (A != (A+1)) { A*=2.0; /*@ ghost i++; */ } /*@ assert A== 0x1.p53; */ }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000657)
cmarche (developer)
2010-02-01 09:51

fixed in Jessie/Why current version
(0000780)
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-02-01 09:42 sboldo New Issue
2010-02-01 09:42 sboldo Status new => assigned
2010-02-01 09:42 sboldo Assigned To => cmarche
2010-02-01 09:46 signoles Assigned To cmarche => virgile
2010-02-01 09:51 cmarche Note Added: 0000657
2010-02-01 09:51 cmarche Assigned To virgile => cmarche
2010-02-01 09:51 cmarche Status assigned => resolved
2010-02-01 09:51 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: 0000780


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker