diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index bf18c353b85083..5766af1fc78a4f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -278,6 +278,11 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { if (const SymbolCast *SC = dyn_cast(Sym)) return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + // UnarySymExpr support is not yet implemented in the Z3 wrapper. + if (isa(Sym)) { + return false; + } + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { if (const SymIntExpr *SIE = dyn_cast(BSE)) return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c new file mode 100644 index 00000000000000..ed9ba72468422e --- /dev/null +++ b/clang/test/Analysis/z3-unarysymexpr.c @@ -0,0 +1,15 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \ +// RUN: -analyzer-constraints=z3 + +// REQUIRES: Z3 +// +// Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate +// that this no longer happens. +// + +// expected-no-diagnostics +int negate(int x, int y) { + if ( ~(x && y)) + return 0; + return 1; +}