Jessie: memory in memeory set

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

---

Id	Project	Category	View	Due Date	Updated
ID0000106	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.)

An uncaugth exception is generated on the followin code:

typedef struct {int i;int j;} las;

/*@ requires \valid(a) && \valid(b); assigns *a, *b; */ void g (int *a,int *b){ *a=11; *b=15; }

/*@ requires \valid(p) ; assigns p->i,p->j; */ void f (las *p) { g (&(p->i), &(p->j)); }

Command line: frama-c.exe -jessie-analysis -jessie-gui foo.c

Error message: memory (mem-field(int_M),b_2) in memory set (mem-field(int_M),a_1), (mem-field(int_M),b_2) File "jc/jc_interp_misc.ml", line 714, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 714, characters 7-13: Assertion failed