diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index bf18c353b85083..16a6b3a2e18112 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -278,6 +278,13 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { if (const SymbolCast *SC = dyn_cast(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 (const UnarySymExpr *USE = dyn_cast(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..80625eb61eb52e --- /dev/null +++ b/clang/test/Analysis/z3-unarysymexpr.c @@ -0,0 +1,16 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \ +// RUN: -analyzer-constraints=z3 + +// REQUIRES: Z3 +// +// This LIT covers a crash associated with this test. +// The expectation is to not crash! +// + +long a; +void b() { + long c; + if (~(b && a)) // expected-warning {{address of function 'b' will always evaluate to 'true'}} + // expected-note@-1 {{prefix with the address-of operator to silence this warning}} + c ^= 0; // expected-warning {{The left expression of the compound assignment is an uninitialized value. The computed value will also be garbage}} +}