NoQ added a comment. In D102696#2766765 <https://reviews.llvm.org/D102696#2766765>, @martong wrote:
> In D102696#2766337 <https://reviews.llvm.org/D102696#2766337>, @NoQ wrote: > >> Ok so the state has enough constraints. It's enough to know that `$x + $y == >> 0` and `$y == 0` in order to deduce that `$x + 0 == 0`. But you're saying >> that we don't know how to infer it so instead of making us able to infer it >> let's make us ask the solver easier questions. That's a terrible hack but at >> this point i think we might as well take it. @vsavchenko WDYT, what would it >> take to fix the solver instead? > > Actually, the problem is more subtle than that. The solver is already capable > of solving such equations, the below test passes on the main branch: > > int test(int x, int y) { > if (y != 0) > return 0; > if (x + y != 0) > return 0; > clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} > clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} > clang_analyzer_eval(x == 0); // expected-warning{{TRUE}} > return 0; > } In this case the equations are `$y == 0` and `$x + 0 == 0` which is much easier to solve. This happens for the same reason that your patch is needed in the first place: we're eagerly substituting a constant. 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
