Currently, if we have a constraint on a binary operator expression and then we add

another constraint to any of the binop's sub-expression then the first

constraint is not considered by the engine:

int foo() { if (x + y != 0) return 0; clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK. if (y != 0) return 0; clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} OK. clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} FAILS! }

Interestingly, if we constrain first y and then (x + y) then the

behaviour is what we'd normally expect:

int foo() { if (y != 0) return 0; if (x + y != 0) return 0; clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK. clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} OK. }

The discrepancy stems from the underlying implementation of the engine:

In the latter case, the Environment of the current ExplodedNode has a

(x + y) -> [0, 0] binding. However, in the first case we have a [y] -> 0

binding in the current ExplodedNode, and when we build the SVal for the

(x + y) expression we simply build up the [x + 0] SVal, i.e. we never

try to find the constraint for (x + y).

In this patch, I add a StmtVisitor that builds up an SVal that

constitutes only from LValue SVals. This SVal then can be used to query

the constraint manager, this way we can find the desired constraint.

Alternative implementation could have been to traverse back in the

Exploded Graph to the Node where we can find the original binding of the

x + y expression. This seemed to be a far from ideal approach as we may

not know how far should we traverse back.