[PATCH] D112296: [Analyzer][solver] Handle adjustments in constraint assignor remainder

[Gabor Marton via Phabricator via cfe-commits]

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


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1623
     if (!Constraint.containsZero()) {
-      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+      State = RCM.assumeSymRel(State, LHS, BO_NE, Zero);
       if (!State)
----------------
ASDenysPetrov wrote:
> What I see, you're still trying to avoid using `State->assume`, which I recommend in a parent revision, but coming closer using its guts.
So, it would look like this:
```
State = State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);
```
The main  reason why we cannot use `State->assume` is that it boils down to `RangedConstraintManager::assumeSym` that has a specific logic for the `boolean` assumption. I.e. the operator is being negated in a case:
```
    if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
      if (!Assumption)
        op = BinaryOperator::negateComparisonOp(op);

      return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
    }
```
You can try it for yourself, and see that the test case added in this patch will not pass if we were to use `State->assume`. Essentially, we have to evade the special "bool" logic, and the closest we can get is using `assumeSymRel`.

Besides that, by using `State->assume` we would have a superfluous conversion chain `Symbol->SVal->Symbol` until we reach `assumeSymRel`. 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112296