0000060: Conversion from integer to real - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000060

Frama-C

Kernel

public

2009-04-23 20:04

2014-02-12 16:56

Reporter

gmelquio

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000060: Conversion from integer to real

Description

While 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?

Tags

No tags attached.

Attached Files

Relationships

related to

0000062

closed

virgile

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