diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h index 7f25223d232cf..b0673b62efffe 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -456,17 +456,15 @@ class SMTConv { llvm::SMTExprRef OperandExp = getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison); - if (const BinarySymExpr *BSE = - dyn_cast(USE->getOperand())) { - if (USE->getOpcode() == UO_Minus && - BinaryOperator::isComparisonOp(BSE->getOpcode())) - // The comparison operator yields a boolean value in the Z3 - // language and applying the unary minus operator on a boolean - // crashes Z3. However, the unary minus does nothing in this - // context (a number is truthy if and only if its negative is - // truthy), so let's just ignore the unary minus. - // TODO: Replace this with a more general solution. - return OperandExp; + // When the operand is a bool expr, but the operator is an integeral + // operator, casting the bool expr to the integer before creating the + // unary operator. + // E.g. -(5 && a) + if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy && + (*RetTy)->isIntegerType()) { + OperandExp = fromCast(Solver, OperandExp, (*RetTy), + Ctx.getTypeSize(*RetTy), OperandTy, 1); + OperandTy = (*RetTy); } llvm::SMTExprRef UnaryExp = diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c index 89c043e5befab..82b0fc988a383 100644 --- a/clang/test/Analysis/z3-unarysymexpr.c +++ b/clang/test/Analysis/z3-unarysymexpr.c @@ -47,3 +47,11 @@ int z3_crash2(int a) { return *d; // expected-warning{{Dereference of undefined pointer value}} return 0; } + +// Refer to issue 165779 +void z3_crash3(long a) { + if (~-(5 && a)) { + long *c; + *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}} + } +}