diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -255,6 +255,20 @@ llvm_unreachable("Unimplemented opcode"); } + static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const llvm::SMTExprRef &Exp, + const UnaryOperator::Opcode Op) { + switch (Op) { + case UO_Minus: + return Solver->mkBVNeg(Exp); + case UO_Not: + return Solver->mkBVNot(Exp); + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, /// and their bit widths. static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, @@ -446,6 +460,17 @@ return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType()); } + if (const UnarySymExpr *USE = dyn_cast(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + QualType FromTy; + llvm::SMTExprRef Exp = + getSymExpr(Solver, Ctx, USE->getOperand(), &FromTy, hasComparison); + + return fromUnary(Solver, Ctx, Exp, USE->getOpcode()); + } + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { llvm::SMTExprRef Exp = getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); diff --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c --- a/clang/test/Analysis/z3-crosscheck.c +++ b/clang/test/Analysis/z3-crosscheck.c @@ -14,6 +14,20 @@ return 0; } +int unary(int x, long l) +{ + int *z = 0; + int y = l; + if ((x & 1) && ((x & 1) ^ 1)) + if (-y) +#ifdef NO_CROSSCHECK + return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}} +#else + return *z; // no-warning +#endif + return 0; +} + void g(int d); void f(int *a, int *b) {