Index: include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -172,41 +172,50 @@ virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) = 0; virtual ProgramStateRef assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0; + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) = 0; //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===// private: static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); + static void computeScale(SymbolRef &Sym, llvm::APFloat &Scale); }; } // end GR namespace Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -250,35 +250,43 @@ ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &V, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) override; ProgramStateRef assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) override; + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) override; private: RangeSet::Factory F; @@ -289,20 +297,27 @@ RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment); RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment); RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment); RangeSet getSymLERange(llvm::function_ref RS, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment); RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment); + llvm::APSInt rescale(const llvm::APSInt &Int, + const llvm::APFloat &Scale) const; }; } // end anonymous namespace @@ -508,6 +523,18 @@ return nullptr; } +llvm::APSInt RangeConstraintManager::rescale(const llvm::APSInt &Int, + const llvm::APFloat &Scale) const { + llvm::APFloat Float(llvm::APFloat::IEEEquad(), + llvm::APFloat::uninitializedTag()); + Float.convertFromAPInt(Int, Int.isSigned(), llvm::APFloat::rmTowardZero); + llvm::APSInt Result(Int.getBitWidth(), Int.isUnsigned()); + bool Exact; + (Float / Scale).convertToInteger(Result, llvm::APFloat::rmTowardZero, &Exact); + + return Result; +} + //===------------------------------------------------------------------------=== // assumeSymX methods: protected interface for RangeConstraintManager. //===------------------------------------------------------------------------===/ @@ -523,18 +550,20 @@ ProgramStateRef RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) return St; - llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment; + llvm::APSInt ScInt = rescale(Int, Scale); + llvm::APSInt Lower = AdjustmentType.convert(ScInt) - Adjustment; llvm::APSInt Upper = Lower; --Lower; ++Upper; - // [Int-Adjustment+1, Int-Adjustment-1] + // [Int/Scale-Adjustment+1, Int/Scale-Adjustment-1] // Notice that the lower bound is greater than the upper bound. RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower); return New.isEmpty() ? nullptr : St->set(Sym, New); @@ -543,14 +572,16 @@ ProgramStateRef RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) return nullptr; - // [Int-Adjustment, Int-Adjustment] - llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; + // [Int/Scale-Adjustment, Int/Scale-Adjustment] + llvm::APSInt ScInt = rescale(Int, Scale); + llvm::APSInt AdjInt = AdjustmentType.convert(ScInt) - Adjustment; RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); return New.isEmpty() ? nullptr : St->set(Sym, New); } @@ -558,6 +589,7 @@ RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); @@ -570,8 +602,10 @@ return getRange(St, Sym); } - // Special case for Int == Min. This is always false. - llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); + llvm::APSInt ScInt = rescale(Int, Scale); + + // Special case for ScInt == Min. This is always false. + llvm::APSInt ComparisonVal = AdjustmentType.convert(ScInt); llvm::APSInt Min = AdjustmentType.getMinValue(); if (ComparisonVal == Min) return F.getEmptySet(); @@ -586,14 +620,16 @@ ProgramStateRef RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { - RangeSet New = getSymLTRange(St, Sym, Int, Adjustment); + RangeSet New = getSymLTRange(St, Sym, Int, Scale, Adjustment); return New.isEmpty() ? nullptr : St->set(Sym, New); } RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); @@ -606,8 +642,10 @@ return F.getEmptySet(); } - // Special case for Int == Max. This is always false. - llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); + llvm::APSInt ScInt = rescale(Int, Scale); + + // Special case for ScInt == Max. This is always false. + llvm::APSInt ComparisonVal = AdjustmentType.convert(ScInt); llvm::APSInt Max = AdjustmentType.getMaxValue(); if (ComparisonVal == Max) return F.getEmptySet(); @@ -622,14 +660,16 @@ ProgramStateRef RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { - RangeSet New = getSymGTRange(St, Sym, Int, Adjustment); + RangeSet New = getSymGTRange(St, Sym, Int, Scale, Adjustment); return New.isEmpty() ? nullptr : St->set(Sym, New); } RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); @@ -642,8 +682,10 @@ return F.getEmptySet(); } - // Special case for Int == Min. This is always feasible. - llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); + llvm::APSInt ScInt = rescale(Int, Scale); + + // Special case for ScInt == Min. This is always feasible. + llvm::APSInt ComparisonVal = AdjustmentType.convert(ScInt); llvm::APSInt Min = AdjustmentType.getMinValue(); if (ComparisonVal == Min) return getRange(St, Sym); @@ -658,14 +700,16 @@ ProgramStateRef RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { - RangeSet New = getSymGERange(St, Sym, Int, Adjustment); + RangeSet New = getSymGERange(St, Sym, Int, Scale, Adjustment); return New.isEmpty() ? nullptr : St->set(Sym, New); } RangeSet RangeConstraintManager::getSymLERange( llvm::function_ref RS, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { // Before we do any real work, see if the value can even show up. APSIntType AdjustmentType(Adjustment); @@ -678,8 +722,10 @@ return RS(); } - // Special case for Int == Max. This is always feasible. - llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); + llvm::APSInt ScInt = rescale(Int, Scale); + + // Special case for ScInt == Max. This is always feasible. + llvm::APSInt ComparisonVal = AdjustmentType.convert(ScInt); llvm::APSInt Max = AdjustmentType.getMaxValue(); if (ComparisonVal == Max) return RS(); @@ -694,33 +740,38 @@ RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { - return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment); + return getSymLERange([&] { return getRange(St, Sym); }, Int, Scale, + Adjustment); } ProgramStateRef RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym, const llvm::APSInt &Int, + const llvm::APFloat &Scale, const llvm::APSInt &Adjustment) { - RangeSet New = getSymLERange(St, Sym, Int, Adjustment); + RangeSet New = getSymLERange(St, Sym, Int, Scale, Adjustment); return New.isEmpty() ? nullptr : St->set(Sym, New); } ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) { - RangeSet New = getSymGERange(State, Sym, From, Adjustment); + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) { + RangeSet New = getSymGERange(State, Sym, From, Scale, Adjustment); if (New.isEmpty()) return nullptr; - RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment); + RangeSet Out = getSymLERange([&] { return New; }, To, Scale, Adjustment); return Out.isEmpty() ? nullptr : State->set(Sym, Out); } ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, const llvm::APSInt &Adjustment) { - RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment); - RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment); + const llvm::APSInt &To, const llvm::APFloat &Scale, + const llvm::APSInt &Adjustment) { + RangeSet RangeLT = getSymLTRange(State, Sym, From, Scale, Adjustment); + RangeSet RangeGT = getSymGTRange(State, Sym, To, Scale, Adjustment); RangeSet New(RangeLT.addRange(F, RangeGT)); return New.isEmpty() ? nullptr : State->set(Sym, New); } Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -77,6 +77,9 @@ BasicValueFactory &BVF = getBasicVals(); APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); + llvm::APFloat Scale = llvm::APFloat(llvm::APFloat::IEEEquad(), 1); + computeScale(Sym, Scale); + llvm::APSInt Adjustment = WraparoundType.getZeroValue(); SymbolRef AdjustedSym = Sym; computeAdjustment(AdjustedSym, Adjustment); @@ -93,9 +96,9 @@ if (InRange) return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom, - ConvertedTo, Adjustment); + ConvertedTo, Scale, Adjustment); return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom, - ConvertedTo, Adjustment); + ConvertedTo, Scale, Adjustment); } ProgramStateRef @@ -110,10 +113,11 @@ // Reverse the operation and add directly to state. const llvm::APSInt &Zero = BVF.getValue(0, T); + const llvm::APFloat One = llvm::APFloat(llvm::APFloat::IEEEquad(), 1); if (Assumption) - return assumeSymNE(State, Sym, Zero, Zero); + return assumeSymNE(State, Sym, Zero, One, Zero); else - return assumeSymEQ(State, Sym, Zero, Zero); + return assumeSymEQ(State, Sym, Zero, One, Zero); } ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State, @@ -138,8 +142,19 @@ BasicValueFactory &BVF = getBasicVals(); APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); - // We only handle simple comparisons of the form "$sym == constant" - // or "($sym+constant1) == constant2". + // We only handle simple comparisons of the form "$sym == constant", + // "($sym*constant0) == constant2" or "($sym+constant1) == constant2". + // FIXME: On the long term support first-degree expressions of + // "($sym*constant0)+constant1 == constant2" + + // The scale is "constant0" in the above expression. It's used to + // "rescale" the solution range. It's up to the subclasses of + // SimpleConstraintManager to handle the scaling. + + + llvm::APFloat Scale = llvm::APFloat(llvm::APFloat::IEEEquad(), 1); + computeScale(Sym, Scale); + // The adjustment is "constant1" in the above expression. It's used to // "slide" the solution range around for modular arithmetic. For example, // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which @@ -162,25 +177,47 @@ llvm_unreachable("invalid operation not caught by assertion above"); case BO_EQ: - return assumeSymEQ(State, Sym, ConvertedInt, Adjustment); + return assumeSymEQ(State, Sym, ConvertedInt, Scale, Adjustment); case BO_NE: - return assumeSymNE(State, Sym, ConvertedInt, Adjustment); + return assumeSymNE(State, Sym, ConvertedInt, Scale, Adjustment); case BO_GT: - return assumeSymGT(State, Sym, ConvertedInt, Adjustment); + return assumeSymGT(State, Sym, ConvertedInt, Scale, Adjustment); case BO_GE: - return assumeSymGE(State, Sym, ConvertedInt, Adjustment); + return assumeSymGE(State, Sym, ConvertedInt, Scale, Adjustment); case BO_LT: - return assumeSymLT(State, Sym, ConvertedInt, Adjustment); + return assumeSymLT(State, Sym, ConvertedInt, Scale, Adjustment); case BO_LE: - return assumeSymLE(State, Sym, ConvertedInt, Adjustment); + return assumeSymLE(State, Sym, ConvertedInt, Scale, Adjustment); } // end switch } +void RangedConstraintManager::computeScale(SymbolRef &Sym, + llvm::APFloat &Scale) { + // Is it a "($sym*constant1)" expression? + if (const SymIntExpr *SE = dyn_cast(Sym)) { + BinaryOperator::Opcode Op = SE->getOpcode(); + if (Op == BO_Mul || Op == BO_Div) { + Sym = SE->getLHS(); + + // FIXME: We do not yet support multiplication/division by negative + if (SE->getRHS() < 0) + return; + + Scale.convertFromAPInt(SE->getRHS(), SE->getRHS().isSigned(), + llvm::APFloat::rmTowardZero); + + // Don't forget to reciprocate the scale if it's being divided. + if (Op == BO_Div) + Scale = llvm::APFloat(llvm::APFloat::IEEEquad(), 1) / Scale; + } + } +} + void RangedConstraintManager::computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { // Is it a "($sym+constant1)" expression? Index: test/Analysis/constraint_manager_scale.c =================================================================== --- /dev/null +++ test/Analysis/constraint_manager_scale.c @@ -0,0 +1,175 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -verify %s + +void clang_analyzer_eval(int); + +#define UINT_MAX (~0U) +#define INT_MAX (UINT_MAX & (UINT_MAX >> 1)) +#define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1)) + +extern void __assert_fail (__const char *__assertion, __const char *__file, + unsigned int __line, __const char *__function) + __attribute__ ((__noreturn__)); +#define assert(expr) \ + ((expr) ? (void)(0) : __assert_fail (#expr, __FILE__, __LINE__, __func__)) + +void add_ne(int x) { + assert(x + 1 != 3); + clang_analyzer_eval(x == 2); // expected-warning{{FALSE}} + clang_analyzer_eval(x == 3); // expected-warning{{UNKNOWN}} +} + +void sub_ne(int x) { + assert(x - 1 != 1); + clang_analyzer_eval(x == 2); // expected-warning{{FALSE}} + clang_analyzer_eval(x == 1); // expected-warning{{UNKNOWN}} +} + +void mult_ne(int x) { + assert(x * 2 != 4); + clang_analyzer_eval(x == 2); // expected-warning{{FALSE}} + clang_analyzer_eval(x == 4); // expected-warning{{UNKNOWN}} +} + +void div_ne(int x) { + assert(x / 2 != 1); + clang_analyzer_eval(x == 2); // expected-warning{{FALSE}} + clang_analyzer_eval(x == 1); // expected-warning{{UNKNOWN}} +} + +void add_eq(int x) { + assert(x + 1 == 3); + clang_analyzer_eval(x == 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 3); // expected-warning{{FALSE}} +} + +void sub_eq(int x) { + assert(x - 1 == 1); + clang_analyzer_eval(x == 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 1); // expected-warning{{FALSE}} +} + +void mult_eq(int x) { + assert(x * 2 == 4); + clang_analyzer_eval(x == 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 4); // expected-warning{{FALSE}} +} + +void div_eq(int x) { + assert(x / 2 == 1); + clang_analyzer_eval(x == 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 1); // expected-warning{{FALSE}} +} + +void add_lt(int x) { + assert(x < INT_MAX); + assert(x + 1 < 5); + clang_analyzer_eval(x < 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x < 3); // expected-warning{{UNKNOWN}} +} + +void sub_lt(int x) { + assert(x - 1 < 3); + clang_analyzer_eval(x < 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x < 3); // expected-warning{{UNKNOWN}} +} + +void mult_lt(int x) { + assert(x * 2 < 8); + clang_analyzer_eval(x < 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x < 2); // expected-warning{{UNKNOWN}} +} + +void div_lt(int x) { + assert(x / 2 < 2); + clang_analyzer_eval(x < 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x < 2); // expected-warning{{UNKNOWN}} +} + +void add_gt(int x) { + assert(x + 1 > 3); + clang_analyzer_eval(x > 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x > 3); // expected-warning{{UNKNOWN}} +} + +void sub_gt(int x) { + assert(x >= 0); + assert(x - 1 > 1); + clang_analyzer_eval(x > 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x > 3); // expected-warning{{UNKNOWN}} +} + +void mult_gt(int x) { + assert(x * 2 > 4); + clang_analyzer_eval(x > 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x > 3); // expected-warning{{UNKNOWN}} +} + +void div_gt(int x) { + assert(x / 2 > 1); + clang_analyzer_eval(x > 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x > 3); // expected-warning{{UNKNOWN}} +} + +void add_ge(int x) { + assert(x + 1 >= 3); + clang_analyzer_eval(x >= 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x >= 3); // expected-warning{{UNKNOWN}} +} + +void sub_ge(int x) { + assert(x >= 0); + assert(x - 1 >= 1); + clang_analyzer_eval(x >= 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x >= 3); // expected-warning{{UNKNOWN}} +} + +void mult_ge(int x) { + assert(x * 2 >= 4); + clang_analyzer_eval(x >= 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x >= 3); // expected-warning{{UNKNOWN}} +} + +void div_ge(int x) { + assert(x / 2 >= 1); + clang_analyzer_eval(x >= 2); // expected-warning{{TRUE}} + clang_analyzer_eval(x >= 3); // expected-warning{{UNKNOWN}} +} + +void add_le(int x) { + assert(x < INT_MAX); + assert(x + 1 <= 5); + clang_analyzer_eval(x <= 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x <= 3); // expected-warning{{UNKNOWN}} +} + +void sub_le(int x) { + assert(x - 1 <= 3); + clang_analyzer_eval(x <= 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x <= 3); // expected-warning{{UNKNOWN}} +} + +void mult_le(int x) { + assert(x * 2 <= 8); + clang_analyzer_eval(x <= 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x <= 2); // expected-warning{{UNKNOWN}} +} + +void div_le(int x) { + assert(x / 2 <= 2); + clang_analyzer_eval(x <= 4); // expected-warning{{TRUE}} + clang_analyzer_eval(x <= 2); // expected-warning{{UNKNOWN}} +} + +void div_overflow_unsigned(unsigned char x) { + assert(x / 2 <= 200); + clang_analyzer_eval(x == 0); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x == 127); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x == 255); // expected-warning{{UNKNOWN}} +} + +void div_overflow_signed(signed char x) { + assert(x / 2 <= 100); + clang_analyzer_eval(x == -128); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x == 0); // expected-warning{{UNKNOWN}} + clang_analyzer_eval(x == 127); // expected-warning{{UNKNOWN}} +}