--- layout: fc_discuss_archives title: Message 103 from Frama-C-discuss on March 2009 ---
I had a similar problem with this code: #pragma JessieIntegerModel(exact) //@ assigns *q; void Copy(int *p, int *q) { *q = *p; } void foo(int a[]) { Copy(&a[0], &a[1]); } 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 tst4.cloc tst4.jc