Frama-C Bug Tracking System - Frama-C
View Issue Details
0001074Frama-CPlug-in > Evapublic2012-01-28 11:342012-09-19 17:16
yakobowski 
pascal 
normalmajoralways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001074: Imprecise result on almost deterministic program
----- memsetff.c -------- int t[10]; void main (char c) { for (int i=0;i
No tags attached.
Issue History
2012-01-28 11:34yakobowskiNew Issue
2012-01-28 11:34yakobowskiStatusnew => assigned
2012-01-28 11:34yakobowskiAssigned To => pascal
2012-01-28 11:34yakobowskiReproducibilityhave not tried => always
2012-01-28 11:34yakobowskiProduct VersionFrama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2012-01-28 11:43pascalNote Added: 0002636
2012-01-28 12:04yakobowskiNote Added: 0002637
2012-01-28 12:11pascalNote Added: 0002638
2012-01-28 17:18yakobowskiNote Edited: 0002637
2012-01-30 14:11svnCheckin
2012-01-30 14:11svnStatusassigned => resolved
2012-01-30 14:11svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002636)
pascal   
2012-01-28 11:43   
Offsetmaps do not have a lattice structure. Improving things here mean making them worse somewhere else, unless we are careful and make sure that the new treatment is only applied when it gains information, and not when it loses information. Here is a program for which is would be easy to provide a less precise result: int a, b; char t[2]; int main(int c) { t[0] = (int) &a; t[1] = (int) &b; if (c) *(short*)t = 12; } It currently gives: t[0] IN {{ garbled mix of &{a} (origin: Arithmetic {t.c:6}) }} [1] IN {{ garbled mix of &{b} (origin: Arithmetic {t.c:7}) }} But with the wrong change, it could give garbled mix of &{a, b} for both elements in t.
(0002637)
yakobowski   
2012-01-28 12:04   
(edited on: 2012-01-28 17:18)
> Offsetmaps do not have a lattice structure. Sure. The question is now along this line: does choosing one strategy for join in some cases, and another in some other cases, break some invariant of the abstract interpretation mechanism (ie. "sorry, the analysis is precise, bot does no longer converge"), or can we safely improve the heuristics?
(0002638)
pascal   
2012-01-28 12:11   
> does choosing one strategy for join in some cases, and another in some other cases, break some invariant Nothing gets any more broken than it already is, as far as I can tell. The obvious heuristic is when joining [0..15] -> a on the one hand and [0..7] -> b, [8..15] -> c on the other hand, if b and c are included in V_Or_Uninitialized.top_int. A more general heuristic is when b and c's value components are included in V.top_int, and have the same indeterminateness flags.