void test1(int i) {
unsigned short j = i;
if (j < 0) {
int a = j;
clang_analyzer_eval(a < 0); // expected-warning{{FALSE}}
}
}
The condition ‘a < 0’ is evaluated as true by the analyzer (and ‘j < 0’ too). Normally the branch can not be entered at all because ‘j < 0’ can not be true. Is this the correct way of how this should work? It looks like that the variable ‘a’ points to the same memory region as ‘i’ that contains a signed value. The problem does not appear if ‘unsigned int’ is used for ‘j’.
Yup, bug. We re-use the same symbol for 'i', 'j', and 'a'. The correct behavior would be to construct a SymbolCast<reg_$0<int i>, unsigned
and then another SymbolCast<SymbolCast<reg_$0<int i>, unsigned , int>.
But it causes more harm than good due to RangeConstraintManager being unable to reason about cast symbols anyway. So, like even if we construct those cast symbols, we'll produce more false positives than we suppress, unless we also improve the constraint solver dramatically. Been there, seen that.
We could do this with Z3 or another full-featured SMT solver, but it probably won't come completely for free with cross-check, as we'll end up exploring more paths (RangeConstraintManager will fail to discard the path immediately more often) and find less bugs (as RangeConstraintManager will fail to discard the non-buggy state more often). I don't have concrete for this particular take on the problem though.