Frama-C Bug Tracking System - Frama-C
View Issue Details
0001264Frama-CPlug-in > Evapublic2012-08-08 13:312013-04-19 11:05
yakobowski 
yakobowski 
lowtweakalways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Fluorine-20130401 
0001264: Locations.valid_enumerate_bits enumerate invalid bits
The 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
The problem lies either in valid_enumerate_bits itself, or in Lattice_Interval_Set.from_ival_int
No tags attached.
Issue History
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:57svnCheckin
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

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