ID0000039: **This issue was created automatically from Mantis Issue 39. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000039 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-11-24 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - | ### Description : [bug 7548 from old bts, reported by Dillon Pariente] Hello, (Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".) Launching: frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c with foo.c containing: //***************************************** typedef struct {int i;int j;} las; /*@ requires \valid(a) && \valid(b); assigns *a, *b; */ void g (int *a,int *b){ *a=11; *b=15; } /*@ requires \valid(p) ; assigns p->i,p->j; */ void f (las *p) { g (&(p->i), &(p->j)); } //***************************************** returns the following error (Jessie/Why version is 2.18): memory (mem-field(int_M),b_21) in memory set (mem-field(int_M),a_20), (mem-field(int_M),b_21) File "jc/jc_interp_misc.ml", line 716, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jc