[PATCH] D103317: [Analyzer][Core] Make SValBuilder to better simplify svals with 3 symbols in the tree

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

Still looks great.



================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:75
+      if (b * b == 1)
+        ; // no-crash (assertion should not be violated)
+  }
----------------
martong wrote:
> steakhal wrote:
> > I guess, this statement should not be reachable.
> > Please demonstrate it by using the `clang_analyzer_WarnIfReached()`.
> Actually, L72 simplifies to `1 != b`, L73 simplifies to the same, L74 is `b ^ 2 == 1`. And this system has a solution: `b == -1` satisfies both L72 and L74 conditions.
> So, this line is reachable, correctly and I've updated the test case like so.
> 
> Note that, however, the ConstraintAssignor is not smart enough to deduce that `b == -1`. I have a WIP branch to accomplish that [[ https://github.com/martong/llvm-project/commit/ed7af2938789c8d2efea7f21b37c6da2d3580d9e | here ]].
Uh, you are right. Thanks.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103317/new/

https://reviews.llvm.org/D103317