[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

> Suppose we have found the way to handle it. But what if we find a contradiction while simplifying, like (short)(int x) = 0 and (int x) = 1. So that we would already know that it is impossible. What SVal should we return in such case? Undef? Unknown? Original one?

I think the `SValBuilder` should not reach such an ambiguity. Ideally, both `(short)(int x)` and `(int x)` should be constrained to the same value. If that is not the case then we already have an infeasible state. But it should not be the task of the SValBuilder to recognize this situation. So, when we add the second constraint **then** we should notice the contradiction immediately. This check should be done in the `ConstraintAssignor`.

> What we could do is to collect the constants and types on the way of the cast visitation and then apply the same logic that you have in D103096 <https://reviews.llvm.org/D103096>

I don't think anymore that this is would be the way forward, as I said, let's do the check for infeasibility in the ConstraintAssignor.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D126481