[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.

I think it looks greatt
There are a couple questions you need to think about, but I don't insist about changing anything if the code works passed widescale testing.



================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:463
+      // has a different type than the unary itself.
+      if (OperandTy != Sym->getType()) {
+        if (hasComparison)
----------------
Could this fail spuriously due to a constness mismatch, since you compare QualTypes instead of types?
What happens if one of these refers to typedef? 
Shouldn't we compare the canonical type pointers instead? Or this works out just fine in practice. I might over-worry this :D

ALternatively, we could emit this cast only if the bitwidths are different. (which caused the sort difference, thus the crash)


================
Comment at: clang/test/Analysis/unary-sym-expr-z3-refutation.c:28
+void k(long L) {
+  int g = L;
+  int h = g + 1;
----------------
So this is the implicit cast that we don't emit.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D125547