Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000117Frama-CKernelpublic2009-06-05 11:162009-06-23 18:03
Reportersboldo 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000117: int -> integer -> real
DescriptionFrom ACSL, I assume that
"C integral types char , short , int and long , signed or unsigned, are all subtypes of type integer ;
 integer is itself a subtype of type real ;"

Therefore int is a subtype of real. But it does not work in practice:

  int i;
  /*@ loop invariant C== \pow(2., i) */

\pow takes 2 real numbers.
This annotation is refused by the message:

Error during analysis of annotation: invalid implicit conversion from int to real

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-06-05 11:16 sboldo New Issue
2009-06-05 11:51 signoles Status new => assigned
2009-06-05 11:51 signoles Assigned To => virgile
2009-06-08 17:05 svn Checkin
2009-06-08 17:05 svn Status assigned => resolved
2009-06-08 17:05 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