[PATCH] D102696: [Analyzer] Find constraints that are directly attached to a BinOp

[Valeriy Savchenko via Phabricator via cfe-commits]

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