ddcc added a comment.
Compared with https://reviews.llvm.org/D28953, this revision fixes the test
failure with `PR3991.m` with RangeConstraintManager, and a few other failures
with Z3ConstraintManager. However, there's one remaining test failure in
`range_casts.c` that I'm not sure how to resolve. For reference, this is the
simplified code snippet from that testcase:
void f15(long foo) {
unsigned index = -1;
if (index < foo) index = foo;
unsigned int tmp = index + 1;
if (tmp == 0)
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
else
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
In debug mode, an assertion about the system being over-constrained is thrown
from `ConstraintManager.h`. This is because the new
`Simplifier::VisitSymbolCast` function will attempt to evaluate the cast
`(unsigned int) (reg_$0<long foo>)`, which is suppressed by the call to
`haveSameType()` in `SimpleSValBuilder::evalCastFromNonLoc`
(https://reviews.llvm.org/D28955 fixes this, but only for Z3ConstraintManager),
generating just the symbol `reg_$0<long foo>`. Subsequently, the analyzer will
attempt to evaluate the expression `((reg_$0<long foo>) + 1U) == 0U` with the
range `reg_$0<long foo> : { [4294967296, 9223372036854775807] }`, or `[UINT_MAX
+ 1, LONG_MAX]`. However, in the case where the assumption is true,
RangeConstraintManager takes the intersection of the previous range with
`[UINT_MAX, UINT_MAX]` and produces the empty set, and likewise where the
assumption is false, the intersection with `[UINT_MAX - 1, 0]` again produces
the empty set. As a result, both program states are NULL, triggering the
assertion.
I'm now somewhat inclined to drop the addition of
`Simplified::VisitSymbolCast()` and those associated testsuite changes, because
ignoring type casts is clearly incorrect and will introduce both false
negatives and false positives.
https://reviews.llvm.org/D35450
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
