Range verification in 2D-array fails

ID0001428: This issue was created automatically from Mantis Issue 1428. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001428	Frama-C	Plug-in > wp	public	2013-05-24	2013-05-24

Reporter	Allan Blanchard	Assigned To	correnson	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130501	Target Version	-	Fixed in Version	-

Description :

Just consider this little example :

void func(){ int a[5][5]; // This works : //@ assert \valid(a[0 .. 4]); //@ assert \valid(&a[0 .. 4][0 .. 4]);

// OK : //@ assert \valid(&a[0][0 .. 4]);

//@ assert \valid(&a[1][0]); //works with 1, 2, 3, 4 but //@ assert \valid(&a[1][0 .. 4]); //does not }