0000386: int32 and real can't be unified - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000386

Frama-C

Plug-in > jessie

public

2010-02-01 09:42

2010-04-19 16:14

Reporter

sboldo

Assigned To

cmarche

Priority

normal

Severity

minor

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 Boron-20100401

Summary

0000386: int32 and real can't be unified

Description

Hello,

With the svn version of frama-c and jessie, I have the following problem: an integer cannot be promoted to real inside a function call.

The function \pow takes 2 real numbers. If I give it an int32. Jessie fails to type it.

Additional Information

# pragma JessieFloatModel(strict)

double malcolm1() {
  double A;
  A=2.0;
  /*@ assert A==2.; */
  /*@ ghost int i = 1; */

  /*@ loop invariant A== \pow(2.,i) &&
    @ 1 <= i <= 53;
    @ loop variant (53-i); */

  while (A != (A+1)) {
    A*=2.0;
    /*@ ghost i++; */
  }

  /*@ assert A== 0x1.p53; */

}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000657) cmarche (developer) 2010-02-01 09:51	fixed in Jessie/Why current version

(0000780) signoles (manager) 2010-04-19 16:14	Fix in Why 2.24 (require Frama-C Boron-20100401).

Issue History
Date Modified	Username	Field	Change
2010-02-01 09:42	sboldo	New Issue
2010-02-01 09:42	sboldo	Status	new => assigned
2010-02-01 09:42	sboldo	Assigned To	=> cmarche
2010-02-01 09:46	signoles	Assigned To	cmarche => virgile
2010-02-01 09:51	cmarche	Note Added: 0000657
2010-02-01 09:51	cmarche	Assigned To	virgile => cmarche
2010-02-01 09:51	cmarche	Status	assigned => resolved
2010-02-01 09:51	cmarche	Resolution	open => fixed
2010-04-19 16:13	signoles	Status	resolved => closed
2010-04-19 16:13	signoles	Fixed in Version	=> Frama-C Boron
2010-04-19 16:14	signoles	Note Added: 0000780