martong added a comment.
In D102696#2768857 <https://reviews.llvm.org/D102696#2768857>, @vsavchenko
wrote:
> 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}} ?
> }
I've added a test case for this, and it passes with the patch.
Also, I added another test case for checking that "y + x" should be zero if "x
+ y" is constrained. This fails. To support that we should be synthesizing all
combination of the commutative expressions, which would not scale of course.
(Perhaps we could do this only for the upper level expression and this way, the
most common case could be supported)
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
