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

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added inline comments.


================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:75
+      if (b * b == 1)
+        ; // no-crash (assertion should not be violated)
+  }
----------------
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 ]].


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317