[clang] [analyzer] Indicate UnarySymExpr is not supported by Z3 (PR #108900)
DonĂ¡t Nagy via cfe-commits
cfe-commits at lists.llvm.org
Thu Sep 19 04:36:16 PDT 2024
================
@@ -278,6 +278,13 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+ // If a UnarySymExpr is encountered, the Z3
+ // wrapper does not support those. So indicate Z3 does not
+ // support those and return.
----------------
NagyDonat wrote:
```suggestion
// UnarySymExpr support is not yet implemented in the Z3 wrapper.
```
https://github.com/llvm/llvm-project/pull/108900
More information about the cfe-commits
mailing list