Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:22 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001264Frama-CPlug-in > Evapublic2013-04-19 11:05
Assigned Toyakobowski 
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.


[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




yakobowski (manager)

Will probably be fixed if we merge Lmap and Lmap_bitwise into one implementation. We will inherit validity checks from Lmap/Offsetmap.


yakobowski (manager)

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
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
+Issue History