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 }