martong added a comment.
I don't see this case different to the unary expressions. Consider the unary
minus for example. Let's say, the symbol `a` is constrained to `[1, 1]` and
then `-a` is constrained to `[-2, -2]`. This is clearly an infeasible state and
the analyzer will terminate the path. So, no further call of SValBuilder should
happen from that point. That is, it is meaningless to evaluate `-(-a)` if there
is a contradiction in the constraints that are assigned to the sub-symbols of
the the symbol tree of `-(-a)`.
Here is a test case that demonstrates this (this passes with latest llvm/main):
// RUN: %clang_analyze_cc1 %s \
// RUN: -analyzer-checker=core \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -analyzer-config eagerly-assume=false \
// RUN: -verify
extern void abort() __attribute__((__noreturn__));
#define assert(expr) ((expr) ? (void)(0) : abort())
void clang_analyzer_warnIfReached();
void clang_analyzer_eval(int);
void test(int a, int b) {
assert(-a == -1);
assert(a == 1);
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
clang_analyzer_eval(-(-a) == 1); // expected-warning{{TRUE}}
assert(-b <= -2);
assert(b == 1);
clang_analyzer_warnIfReached(); // unreachable!, no-warning
clang_analyzer_eval(-(-b) == 1); // no-warning
}
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D126481/new/
https://reviews.llvm.org/D126481
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
