vsavchenko added a comment.
My take on this: for whatever approach, we definitely will be able to construct
a more nested/complex example so that it doesn't work.
For this patch, I'm wondering about something like this:
int foo() {
if (z != 0)
return 0;
if (x + y + z != 0)
return 0;
clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} OK.
if (y != 0)
return 0;
clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} OK.
clang_analyzer_eval(z == 0); // expected-warning{{TRUE}} OK.
clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} ?
}
As for the solver, it is something that tormented me for a long time. Is there
a way to avoid a full-blown brute force check of all existing constraints and
get some knowledge about symbolic expressions by constraints these symbolic
expressions are actually part of (right now we can reason about expressions if
we know some information about its own parts aka operands)?
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D102696/new/
https://reviews.llvm.org/D102696
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
