0001074: Imprecise result on almost deterministic program

Notes
(0002636) pascal (reporter) 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 (manager) 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 (reporter) 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.

Issue History
Date Modified	Username	Field	Change
2012-01-28 11:34	yakobowski	New Issue
2012-01-28 11:34	yakobowski	Status	new => assigned
2012-01-28 11:34	yakobowski	Assigned To	=> pascal
2012-01-28 11:34	yakobowski	Reproducibility	have not tried => always
2012-01-28 11:34	yakobowski	Product Version	Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2012-01-28 11:43	pascal	Note Added: 0002636
2012-01-28 12:04	yakobowski	Note Added: 0002637
2012-01-28 12:11	pascal	Note Added: 0002638
2012-01-28 17:18	yakobowski	Note Edited: 0002637
2012-01-30 14:11	svn	Checkin
2012-01-30 14:11	svn	Status	assigned => resolved
2012-01-30 14:11	svn	Resolution	open => fixed
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Relationships