Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000060Frama-CKernelpublic2009-04-23 20:042014-02-12 16:56
Reportergmelquio 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000060: Conversion from integer to real
DescriptionWhile the documentation says that "there are implicit coercions for numeric types: integer is itself a subtype of type real" and that cast are allowed in logic expressions, neither seem to work.

/*@ ensures 1.0 == 1; */
void f();

/*@ ensures 1.0 == (real)1; */
void g();

When running "frama-c test.c" (revision 5096), I get

File test.c, line 1, characters 19-20:
Error during analysis of annotation: invalid cast between real and integer. Use conversion functions instead
test.c:1: Warning: Ignoring specification of function f
File test.c, line 4, characters 19-26:
Error during analysis of annotation: cannot cast to logic type
test.c:4: Warning: Ignoring specification of function g

The error message talks about some "conversion functions", but there are no such things in the documentation. The Jessie plugin seems to know about a \real_of_int function, but the CIL front end does not. So how does one convert an integer to a real, if neither implicit nor explicit casts work?
TagsNo tags attached.
Attached Files

- Relationships
related to 0000062closedvirgile integer is not well-casted in real 

-  Notes
(0000024)
virgile (developer)
2009-04-24 10:36

Casts are only allowed to C types, not to logic types
(e.g, /*@ lemma foo: 1.0 == (float)1; */ will work). The conversion from integer to real should indeed be implicit, though.

- Issue History
Date Modified Username Field Change
2009-04-23 20:04 gmelquio New Issue
2009-04-24 10:30 virgile Status new => assigned
2009-04-24 10:30 virgile Assigned To => virgile
2009-04-24 10:36 virgile Note Added: 0000024
2009-04-24 16:16 virgile Relationship added related to 0000062
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