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 - 2018 MantisBT Team
Powered by Mantis Bugtracker