Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Files

- Relationships

-  Notes
(0003674)
yakobowski (manager)
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 (manager)
2013-02-08 19:45

Original imprecision was indeed in Lattice_Interval_Set.from_ival_int

- Issue History
Date Modified Username Field Change
2012-08-08 13:31 yakobowski New Issue
2012-08-08 13:31 yakobowski Status new => assigned
2012-08-08 13:31 yakobowski Assigned To => pascal
2013-01-25 21:39 yakobowski Assigned To pascal => yakobowski
2013-01-25 21:40 yakobowski Note Added: 0003674
2013-02-08 19:45 yakobowski Note Added: 0003687
2013-02-08 19:57 svn Checkin
2013-02-08 19:57 svn Status assigned => resolved
2013-02-08 19:57 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker