assign makes Jessie crash

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

---

Id	Project	Category	View	Due Date	Updated
ID0000303	Frama-C	Plug-in > jessie	public	2009-10-26	2014-02-12

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

Description :

Code [1] makes Jessie crash [2] on Beryllium-20090901.

[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; }

void Foo() { const int n=10; int a[n]; int i;

for(i=0; i<n; i++) a[i]=0; //@ loop assigns a[0..n-1]; for(i=1; i<n; i++) Swap(&a[i], &a[0]); }

[2] [kernel] preprocessing with "gcc -C -E -I. -dD tst.c" tst.c:17:[kernel] warning: Variable-sized local variable a [jessie] Starting Jessie translation [kernel] No code for function __builtin_alloca, default assigns generated [jessie] Producing Jessie files in subdir tst.jessie [jessie] File tst.jessie/tst.jc written. [jessie] File tst.jessie/tst.cloc written. [jessie] Calling Jessie tool in subdir tst.jessie Generating Why function Swap Generating Why function Foo ** Jc_interp_misc.transpose_location_list: TODO: parameters ** memory (mem-field(int_M),q_4) in memory set (mem-field(int_M),p_3), (mem-field(int_M),q_4) File "jc/jc_interp_misc.ml", line 733, characters 1-1: Uncaught exception: File "jc/jc_interp_misc.ml", line 733, characters 1-7: Assertion failed [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst.cloc tst.jc

Additional Information :

See also bug 80 http://bts.frama-c.com/view.php?id=80