Jessie: float_P[..] expected instead of real

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

---

Id	Project	Category	View	Due Date	Updated
ID0000105	Frama-C	Plug-in > jessie	public	2009-05-27	2009-05-28

Reporter	dpariente	Assigned To	-	Resolution	duplicate
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)

Please, find below the contents of files foo.c and foo.h:

//===== file foo.c typedef struct {float k;} las; void g (float * y); void f (las *c) { g(&(c->k)); }

//===== file foo.h typedef struct {float k;} las; //@ requires \valid(c); assigns c->k; void f (las * c);

command line: frama-c.exe -jessie-analysis -jessie-gui foo.c foo.h

Error message: Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing error: type float_P[..] expected instead of real Jessie subprocess failed: jessie -why-opt -split-user-conj -v -why-opt -fast-wp -separation -locs wholeprogram.cloc w holeprogram.jc