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.