[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware added a comment.

In https://reviews.llvm.org/D35110#1119496, @NoQ wrote:

> Which expressions are constrained? Why does the difference use the whole range? Is it something that could have been fixed by the "enforce that separately" part in my old comment:
>
> > iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], right? So if we subtract one such symbol from another, it's going to be in range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the iterator checker to enforce that separately?
>
> ?


`RangedConstraintManager` currently does not support `Sym+Sym`-type of expressions, only `Sym+Int`-type ones. That is why it cannot calculate that the result is within `[-2³⁰, 2³⁰]`. In the iterator checkers we do not know anything about the rearranged expressions, it has no access to the sum/difference, the whole purpose of your proposal was to put in into the infrastructure. The checker enforces everything it can but it does not help.


https://reviews.llvm.org/D35110