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