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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
