0000062: integer is not well-casted in real - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000062

Frama-C

Kernel

public

2009-04-24 15:58

2014-02-12 16:56

Reporter

sboldo

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000062: integer is not well-casted in real

Description

The 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 Information

Release ID: 5098

Tags

No tags attached.

Relationships

related to

closed

Conversion from integer to real

Notes
(0000026) virgile (developer) 2009-04-24 16:17	likely the same issue as bug #60

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 - 2020 MantisBT Team