Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001264Frama-CPlug-in > Evapublic2012-08-08 13:312013-04-19 11:05
Reporteryakobowski 
Assigned Toyakobowski 
PrioritylowSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001264: Locations.valid_enumerate_bits enumerate invalid bits
DescriptionThe program below shows that valid_enumerate_bits can return Top intervals, even on bases where the validity is completely known. This defeats the purpose of the function, and can cause very subtle bugs with the "default" flag in Offsetmap_bitwise.

---------- many.c ----------------
struct s {
  int f1;
  int f2;
};

struct s t[10][10];

void main() {
  for (int i=0; i<10; i++) {
    for (int j=0; j<10; j++) {
      t[i][j].f1 = 1;
    }
  }
}
-------------------------------------
Command-line: frama-c -val many.c -out -plevel 80 -slevel 50

This combination of slevel/plevel will result in only one " more than foo elements to enumerate. Approximating." message, caused by the Out plugin.

----------------------------------------
Output:

[inout] Out (internal) for function main:
          t[..]; i; j

The expected output is t[0..9][0..9]; i; j



Additional InformationThe problem lies either in valid_enumerate_bits itself, or in Lattice_Interval_Set.from_ival_int
TagsNo tags attached.
Relationships
Attached Files

Notes
(0003674)
yakobowski   
2013-01-25 21:40   
Will probably be fixed if we merge Lmap and Lmap_bitwise into one implementation. We will inherit validity checks from Lmap/Offsetmap.
(0003687)
yakobowski   
2013-02-08 19:45   
Original imprecision was indeed in Lattice_Interval_Set.from_ival_int

Issue History
Date ModifiedUsernameFieldChange
2012-08-08 13:31yakobowskiNew Issue
2012-08-08 13:31yakobowskiStatusnew => assigned
2012-08-08 13:31yakobowskiAssigned To => pascal
2013-01-25 21:39yakobowskiAssigned Topascal => yakobowski
2013-01-25 21:40yakobowskiNote Added: 0003674
2013-02-08 19:45yakobowskiNote Added: 0003687
2013-02-08 19:57svn
2013-02-08 19:57svnStatusassigned => resolved
2013-02-08 19:57svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva