Skip to content

Commit 91e5e83

Browse files
author
git apple-llvm automerger
committed
Merge commit '9ca62c530263' from llvm.org/main into next
2 parents 09753f7 + 9ca62c5 commit 91e5e83

File tree

2 files changed

+20
-0
lines changed

2 files changed

+20
-0
lines changed

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,11 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
278278
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
279279
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
280280

281+
// UnarySymExpr support is not yet implemented in the Z3 wrapper.
282+
if (isa<UnarySymExpr>(Sym)) {
283+
return false;
284+
}
285+
281286
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
282287
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
283288
return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));

clang/test/Analysis/z3-unarysymexpr.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
2+
// RUN: -analyzer-constraints=z3
3+
4+
// REQUIRES: Z3
5+
//
6+
// Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate
7+
// that this no longer happens.
8+
//
9+
10+
// expected-no-diagnostics
11+
int negate(int x, int y) {
12+
if ( ~(x && y))
13+
return 0;
14+
return 1;
15+
}

0 commit comments

Comments
 (0)