martong marked an inline comment as done.
martong added inline comments.
================
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)
----------------
steakhal wrote:
> 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)
> Could this fail spuriously due to a constness mismatch, since you compare
> QualTypes instead of types?
No, I don't think so. The underlying `fromCast` would simply return the same
`SMTExprRef` if the bitwidths are the same.
> What happens if one of these refers to typedef?
The same as in case of the qualifier mismatch.
> 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)
Good point. The code would be more direct and efficient like that, I am going
to update.
================
Comment at: clang/test/Analysis/unary-sym-expr-z3-refutation.c:28
+void k(long L) {
+ int g = L;
+ int h = g + 1;
----------------
steakhal wrote:
> So this is the implicit cast that we don't emit.
Yes.
Actually, without emitting SymbolCasts: `h` is evaluated as `$L<long> + 1`.
However, the expression's type is `int`.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D125547/new/
https://reviews.llvm.org/D125547
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
