diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1614,14 +1614,14 @@ bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) { if (Sym->getOpcode() != BO_Rem) return true; - const SymbolRef LHS = Sym->getLHS(); - const llvm::APSInt &Zero = - Builder.getBasicValueFactory().getValue(0, Sym->getType()); // a % b != 0 implies that a != 0. if (!Constraint.containsZero()) { - State = RCM.assumeSymNE(State, LHS, Zero, Zero); - if (!State) - return false; + SVal SymSVal = Builder.makeSymbolVal(Sym->getLHS()); + if (auto NonLocSymSVal = SymSVal.getAs()) { + State = State->assume(*NonLocSymSVal, true); + if (!State) + return false; + } } return true; } diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -41,7 +41,12 @@ return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS()); } - } else if (const SymSymExpr *SSE = dyn_cast(Sym)) { + // Handle adjustment with non-comparison ops. + const llvm::APSInt &Zero = getBasicVals().getValue(0, SIE->getType()); + return assumeSymRel(State, SIE, (Assumption ? BO_NE : BO_EQ), Zero); + } + + if (const auto *SSE = dyn_cast(Sym)) { BinaryOperator::Opcode Op = SSE->getOpcode(); assert(BinaryOperator::isComparisonOp(Op)); diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c --- a/clang/test/Analysis/constraint-assignor.c +++ b/clang/test/Analysis/constraint-assignor.c @@ -3,9 +3,8 @@ // RUN: -analyzer-checker=debug.ExprInspection \ // RUN: -verify -// expected-no-diagnostics - void clang_analyzer_warnIfReached(); +void clang_analyzer_eval(int); void rem_constant_rhs_ne_zero(int x, int y) { if (x % 3 == 0) // x % 3 != 0 -> x != 0 @@ -67,3 +66,19 @@ if (d % 2 != 0) return; } + +void remainder_with_adjustment(int x) { + if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1 + return; + clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x != -1); // expected-warning{{TRUE}} + (void)x; // keep the constraints alive. +} + +void remainder_with_adjustment_of_composit_lhs(int x, int y) { + if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1 + return; + clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x + y != -1); // expected-warning{{TRUE}} + (void)(x * y); // keep the constraints alive. +}