is_finite predicate: type double expected instead of real in .jc file

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

---

Id	Project	Category	View	Due Date	Updated
ID0000260	Frama-C	Plug-in > jessie	public	2009-09-30	2009-10-15

Reporter	dpariente	Assigned To	ayad	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090902	Target Version	-	Fixed in Version	Frama-C Beryllium-20090902

Description :

Launching: frama-c -jessie foo.c with foo.c containing:

double f(double a , double b ) { double t ; t = 0.0; //@ assert \is_finite((double)(a-b)); t = a - b; return (t); }

yields:

File "foo.jc", line 36, characters 56-71: typing error: type double expected instead of real [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc

":> real" in foo.jc should be removed when used within "is_finite_double" predicate, not?

Regards, Dillon