[clang] [analyzer] Indicate UnarySymExpr is not supported by Z3 (PR #108900)

Mikael Holmén via cfe-commits cfe-commits at lists.llvm.org
Tue Sep 17 23:03:13 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.
+    if (dyn_cast<UnarySymExpr>(Sym)) {
----------------
mikaelholmen wrote:

You can use "isa" here instead of dyn_cast since we're not really using the casted value anyway.

https://github.com/llvm/llvm-project/pull/108900


More information about the cfe-commits mailing list