[PATCH] D110913: [analyzer][solver] Handle simplification to ConcreteInt

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/test/Analysis/solver-sym-simplification-concreteint.c:22
+  // c == 0 --> 0 + 1 == 0 contradiction
+  clang_analyzer_eval(c == 0);    // expected-warning{{FALSE}}
+
----------------
martong wrote:
> steakhal wrote:
> > Could we have an `eval(c == -1) // TRUE`?
> > Also, please disable eager bifurcation to prevent state-splits in the eval arguments.
> Actually,  it is `eval(c == -1) // FALSE` that holds. 
> 
> This is because after the simplification with `b==1` we have a constraint `c+1==0` but we do not reorder this equality to `c==-1`. Besides we have another constraint that we inherited from a previous State, this is `c: [0, 1]`. Now, when you query `c==-1` then the latter constraint is found, thus resulting in an infeasible state, so you'll receive `FALSE` in the warning. Actually, these are the constraints after line 19:
> ```
>   "constraints": [
>     { "symbol": "(reg_$1<int c>) + (reg_$0<int b>)", "range": "{ [0, 0] }" },
>     { "symbol": "(reg_$1<int c>) + 1", "range": "{ [0, 0] }" },
>     { "symbol": "reg_$0<int b>", "range": "{ [1, 1] }" },
>     { "symbol": "reg_$1<int c>", "range": "{ [0, 1] }" }
>   ],
> ```
> 
> I am considering to create a follow-up patch, where the reordering of `c+1==0` to `c==-1` is done (perhaps by reusing `RangedConstraintManager::assumeSymRel`).
I've just updated the test case to be way more direct and simple.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110913