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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

@martong

> So, the intersection should be empty in the above mentioned ambiguous case, shouldn't' it?

No. My current implementation doesn't contain this check in ConstraintAssignor in favor of the solution simplification. It'll be added in the next patches.

But still I think, this solution is not accomplished. Consider next. Say, symbol `(char)(int x)` is associated to the range `[42, 42]`, and can be simplified to constant `42 of char`. And `(int x)` is associated to the range `[43, 43]` Your patch will omit looking into the symbol itself and unwrap it starting visiting the operand instead. Thus, it will return the constant 43 for `(int x)`.
Moreover, if `(int x)` is 43, it will contradict to 42 (aka infeasible state). We also have no decision what to return in this case.

For me, this is really uncertain patch that I'm not 100% sure in.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D126481