Frama-C Bug Tracking System - Frama-C
View Issue Details
0001428Frama-CPlug-in > wppublic2013-05-24 13:352013-05-24 14:15
Allan Blanchard 
correnson 
normalminoralways
assignedopen 
Frama-C Fluorine-20130501 
 
0001428: Range verification in 2D-array fails
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 }
No tags attached.
related to 0001389assigned correnson Translation of tsets 
Issue History
2013-05-24 13:35Allan BlanchardNew Issue
2013-05-24 13:35Allan BlanchardStatusnew => assigned
2013-05-24 13:35Allan BlanchardAssigned To => correnson
2013-05-24 14:14signolesRelationship addedrelated to 0001389
2013-05-24 14:15signolesNote Added: 0003887

Notes
(0003887)
signoles   
2013-05-24 14:15   
It works if you change the last assertion //@ assert \valid(&a[1][0 .. 4]); by the following equivalent one: //@ assert \forall integer i; 0 <= i <= 4 ==> \valid(&a[1][i]); So probably it is the same issue than bts #1389.