2021-03-02 15:27 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000062Frama-CKernelpublic2014-02-12 16:56
Reportersboldo 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 
+Relationships

-Notes

~0000026

virgile (developer)

likely the same issue as bug 0000060
+Notes

-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
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
2013-12-19 01:13 Source_changeset_attached => framac master 96132949
2014-02-12 16:56 Source_changeset_attached => framac stable/neon 96132949
+Issue History