Frama-C/Jessie: memory set problem

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

---

Id	Project	Category	View	Due Date	Updated
ID0000039	Frama-C	Plug-in > jessie	public	2009-04-07	2009-11-24

Reporter	virgile	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

[bug 7548 from old bts, reported by Dillon Pariente] Hello,

(Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".)

Launching: frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c

with foo.c containing:

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

returns the following error (Jessie/Why version is 2.18):

memory (mem-field(int_M),b_21) in memory set (mem-field(int_M),a_20), (mem-field(int_M),b_21) File "jc/jc_interp_misc.ml", line 716, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc