Assertion failed in jc_interp_misc.ml

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

---

Id	Project	Category	View	Due Date	Updated
ID0000080	Frama-C	Plug-in > jessie	public	2009-05-11	2009-11-25

Reporter	boris	Assigned To	cmarche	Resolution	duplicate
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

Jessie crashes on code [1] with error message [2].

Environment: Windows XP, cygwin

---

[1]

/*@ requires \valid(p) && \valid(q); ensures *p == \old(*q); ensures *q == \old(*p); assigns *p, *q; */ void Swap(int *p, int *q) { int temp; temp = *p; *p = *q; *q = temp; }

/*@ requires \valid(a+ (0..k)); */ void foo(int a[], int k) { Swap(&a[0], &a[k]); }

[2]

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

Additional Information :

This bug is likely related to bug 38 http://bts.frama-c.com/view.php?id=38