Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001428Frama-CPlug-in > wppublic2013-05-24 13:352013-05-24 14:15
ReporterAllan Blanchard 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in Version 
Summary0001428: Range verification in 2D-array fails
DescriptionJust 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 }
TagsNo tags attached.
Attached Files

- Relationships
related to 0001389assignedcorrenson Translation of tsets 

-  Notes
(0003887)
signoles (manager)
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.

- Issue History
Date Modified Username Field Change
2013-05-24 13:35 Allan Blanchard New Issue
2013-05-24 13:35 Allan Blanchard Status new => assigned
2013-05-24 13:35 Allan Blanchard Assigned To => correnson
2013-05-24 14:14 signoles Relationship added related to 0001389
2013-05-24 14:15 signoles Note Added: 0003887


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker