Jessie: memory in memeory set
ID0000106: This issue was created automatically from Mantis Issue 106. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000106 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-05-28 |
| Reporter | dpariente | Assigned To | - | Resolution | duplicate |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
An uncaugth exception is generated on the followin code:
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)); }
Command line: frama-c.exe -jessie-analysis -jessie-gui foo.c
Error message: memory (mem-field(int_M),b_2) in memory set (mem-field(int_M),a_1), (mem-field(int_M),b_2) File "jc/jc_interp_misc.ml", line 714, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 714, characters 7-13: Assertion failed