Skip to content
Snippets Groups Projects
user avatar
David Bühler authored
Removes an heuristic that prevented the inference of octagons when the ival
for [x±y] contains all possible values for the type of [x] or [y].
This heuristic was too strong:
- it prevented some inference of relations about unsigned variables, as it also
  checked incorrectly the negation of the given ival;
- it could prevent the inference of relevant relations between signed variables,
  such as 200 < (int)cx + (int)cy < 200 where [cx] and [cy] have char types.

Instead, we now only checks that a new inferred octagon is not redundant with
the interval values, i.e. that the value for [x±y] cannot be computed solely
from the intervals of [x] and [y].
e09106e4
History
Name Last commit Last update
..