int32 and real can't be unified

ID0000386: This issue was created automatically from Mantis Issue 386. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000386	Frama-C	Plug-in > jessie	public	2010-02-01	2010-04-19

Reporter	sboldo	Assigned To	cmarche	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Boron-20100401

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; */

}