Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000062Frama-CKernelpublic2009-04-24 15:582014-02-12 16:56
Reportersboldo 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000062: integer is not well-casted in real
DescriptionThe following program fails with

"Error during analysis of annotation: invalid cast between real and integer. Use conversion functions instead"

But it works with int instead of integer....


/*@ axiomatic toto {
  @ logic integer g;
  @ } */

void f() {
 double B;
/*@ assert B==g; */
}

Additional InformationRelease ID: 5098
TagsNo tags attached.
Attached Files

- Relationships
related to 0000060closedvirgile Conversion from integer to real 

-  Notes
(0000026)
virgile (developer)
2009-04-24 16:17

likely the same issue as bug 0000060

- Issue History
Date Modified Username Field Change
2009-04-24 15:58 sboldo New Issue
2009-04-24 16:16 virgile Relationship added related to 0000060
2009-04-24 16:17 virgile Note Added: 0000026
2009-04-24 16:17 virgile Status new => assigned
2009-04-24 16:17 virgile Assigned To => virgile
2009-04-27 18:43 svn Checkin
2009-04-27 18:43 svn Status assigned => resolved
2009-04-27 18:43 svn Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker