[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

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

steakhal added a comment.

The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.
I'm gonna come back to this tomorrow.



================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:36
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+    return;
----------------
Please express that `C: [-2,-1]` is then intersected with the already associated range which is `[-1,1]`, thus we get `c: [-1,-1]`.


================
Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:55
+  if (b != 1)         // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+    return;
+  clang_analyzer_warnIfReached(); // no warning
----------------
Can we infer within this true branch that `b` must be `0` to make this path feasible?
If we already can infer this, can we put there the appropriate assertion?
If not, an assertion would be justified with a FIXME.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642