array range in requires predicate
ID0000256: This issue was created automatically from Mantis Issue 256. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000256 | Frama-C | Plug-in > jessie | public | 2009-09-25 | 2009-09-25 |
Reporter | jcrown | Assigned To | cmarche | Resolution | open |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
frama-c -main foo file.c -jessie
on code typedef struct { int a; } A; typedef struct { A * c[10]; } B; typedef struct { B * c[10]; } C; C v; /@......./ void foo(void);
wth one of the 3 contracts below on foo() /*@ requires \valid((v.c[0 .. 9])->c[0 .. 9]); / /@ requires \valid((v.c[0 .. 9])->c+(0 .. 9)); / /@ requires \valid((v.c+(0 .. 9))->c+(0 .. 9)); */
->
Uncaught exception: File "jc/jc_interp.ml", line 939, characters 25-31: Assertion failed on the 1st and 2nd ones,
and file.c:8:[kernel] user error: Error during annotations analysis: expected a struct with field c on the 3rd one.