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