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 @@ -1347,27 +1347,35 @@ // Equality tracking implementation //===------------------------------------------------------------------===// - ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &Int, + ProgramStateRef trackEQ(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { - if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { - // Extract function assumes that we gave it Sym + Adjustment != Int, - // so the result should be opposite. - Equality->invert(); - return track(State, *Equality); - } - - return State; + return track(NewConstraint, State, Sym, Int, Adjustment); } - ProgramStateRef trackNE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &Int, + ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { + return track(NewConstraint, State, Sym, Int, Adjustment); + } + + template + ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State, + SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APSInt &Adjustment) { + if (NewConstraint.isEmpty()) + // This is an infeasible assumption. + return nullptr; + + ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint); if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { - return track(State, *Equality); + // If the original assumption is not Sym + Adjustment !=/ Int, + // we should invert IsEquality flag. + Equality->IsEquality = Equality->IsEquality != EQ; + return track(NewState, *Equality); } - return State; + return NewState; } ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) { @@ -2042,12 +2050,7 @@ RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point); - if (New.isEmpty()) - // this is infeasible assumption - return nullptr; - - ProgramStateRef NewState = setConstraint(St, Sym, New); - return trackNE(NewState, Sym, Int, Adjustment); + return trackNE(New, St, Sym, Int, Adjustment); } ProgramStateRef @@ -2063,12 +2066,7 @@ llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); - if (New.isEmpty()) - // this is infeasible assumption - return nullptr; - - ProgramStateRef NewState = setConstraint(St, Sym, New); - return trackEQ(NewState, Sym, Int, Adjustment); + return trackEQ(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St, @@ -2104,7 +2102,7 @@ const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymLTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St, @@ -2140,7 +2138,7 @@ const llvm::APSInt &Int, const llvm::APSInt &Adjustment) { RangeSet New = getSymGTRange(St, Sym, Int, Adjustment); - return New.isEmpty() ? nullptr : setConstraint(St, Sym, New); + return trackNE(New, St, Sym, Int, Adjustment); } RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St, diff --git a/clang/test/Analysis/equality_tracking.c b/clang/test/Analysis/equality_tracking.c --- a/clang/test/Analysis/equality_tracking.c +++ b/clang/test/Analysis/equality_tracking.c @@ -185,3 +185,37 @@ } } } + +void avoidInfeasibleConstraintforGT(int a, int b) { + int c = b - a; + if (c <= 0) + return; + // c > 0 + // b - a > 0 + // b > a + if (a != b) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + return; + } + clang_analyzer_warnIfReached(); // no warning + // a == b + if (c < 0) + ; +} + +void avoidInfeasibleConstraintforLT(int a, int b) { + int c = b - a; + if (c >= 0) + return; + // c < 0 + // b - a < 0 + // b < a + if (a != b) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + return; + } + clang_analyzer_warnIfReached(); // no warning + // a == b + if (c < 0) + ; +}