Index: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h @@ -312,6 +312,9 @@ /// \sa shouldDisplayNotesAsEvents Optional DisplayNotesAsEvents; + /// \sa shouldAggressivelySimplifyRelationalComparison + Optional AggressiveRelationalComparisonSimplification; + /// \sa getCTUDir Optional CTUDir; @@ -666,6 +669,20 @@ /// to false when unset. bool shouldDisplayNotesAsEvents(); + /// Returns true if SValBuilder should rearrange comparisons of symbolic + /// expressions which consist of a sum of a symbol and a concrete integer + /// into the format where symbols are on the left-hand side and the integer + /// is on the right. This is only done if both symbols and both concrete + /// integers are signed, greater than or equal to the quarter of the minimum + /// value of the type and less than or equal to the quarter of the maximum + /// value of that type. + /// + /// A + n B + m becomes A - B m - n, where A and B symbolic, + /// n and m are integers. is any of '==', '!=', '<', '<=', '>' or '>='. + /// The rearrangement also happens with '-' instead of '+' on either or both + /// side and also if any or both integers are missing. + bool shouldAggressivelySimplifyRelationalComparison(); + /// Returns the directory containing the CTU related files. StringRef getCTUDir(); Index: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp @@ -445,6 +445,14 @@ return DisplayNotesAsEvents.getValue(); } +bool AnalyzerOptions::shouldAggressivelySimplifyRelationalComparison() { + if (!AggressiveRelationalComparisonSimplification.hasValue()) + AggressiveRelationalComparisonSimplification = + getBooleanOption("aggressive-relational-comparison-simplification", + /*Default=*/false); + return AggressiveRelationalComparisonSimplification.getValue(); +} + StringRef AnalyzerOptions::getCTUDir() { if (!CTUDir.hasValue()) { CTUDir = getOptionAsString("ctu-dir", ""); Index: cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp @@ -12,8 +12,10 @@ //===----------------------------------------------------------------------===// #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h" using namespace clang; @@ -307,6 +309,192 @@ return makeNonLoc(LHS, op, *ConvertedRHS, resultTy); } +// See if Sym is known to be a relation Rel with Bound. +static bool isInRelation(BinaryOperator::Opcode Rel, SymbolRef Sym, + llvm::APSInt Bound, ProgramStateRef State) { + SValBuilder &SVB = State->getStateManager().getSValBuilder(); + SVal Result = + SVB.evalBinOpNN(State, Rel, nonloc::SymbolVal(Sym), + nonloc::ConcreteInt(Bound), SVB.getConditionType()); + if (auto DV = Result.getAs()) { + return !State->assume(*DV, false); + } + return false; +} + +// See if Sym is known to be within [min/4, max/4], where min and max +// are the bounds of the symbol's integral type. With such symbols, +// some manipulations can be performed without the risk of overflow. +// assume() doesn't cause infinite recursion because we should be dealing +// with simpler symbols on every recursive call. +static bool isWithinConstantOverflowBounds(SymbolRef Sym, + ProgramStateRef State) { + SValBuilder &SVB = State->getStateManager().getSValBuilder(); + BasicValueFactory &BV = SVB.getBasicValueFactory(); + + QualType T = Sym->getType(); + assert(T->isSignedIntegerOrEnumerationType() && + "This only works with signed integers!"); + APSIntType AT = BV.getAPSIntType(T); + + llvm::APSInt Max = AT.getMaxValue() / AT.getValue(4), Min = -Max; + return isInRelation(BO_LE, Sym, Max, State) && + isInRelation(BO_GE, Sym, Min, State); +} + +// Same for the concrete integers: see if I is within [min/4, max/4]. +static bool isWithinConstantOverflowBounds(llvm::APSInt I) { + APSIntType AT(I); + assert(!AT.isUnsigned() && + "This only works with signed integers!"); + + llvm::APSInt Max = AT.getMaxValue() / AT.getValue(4), Min = -Max; + return (I <= Max) && (I >= -Max); +} + +static std::pair +decomposeSymbol(SymbolRef Sym, BasicValueFactory &BV) { + if (const auto *SymInt = dyn_cast(Sym)) + if (BinaryOperator::isAdditiveOp(SymInt->getOpcode())) + return std::make_pair(SymInt->getLHS(), + (SymInt->getOpcode() == BO_Add) ? + (SymInt->getRHS()) : + (-SymInt->getRHS())); + + // Fail to decompose: "reduce" the problem to the "$x + 0" case. + return std::make_pair(Sym, BV.getValue(0, Sym->getType())); +} + +// Simplify "(LSym + LInt) Op (RSym + RInt)" assuming all values are of the +// same signed integral type and no overflows occur (which should be checked +// by the caller). +static NonLoc doRearrangeUnchecked(ProgramStateRef State, + BinaryOperator::Opcode Op, + SymbolRef LSym, llvm::APSInt LInt, + SymbolRef RSym, llvm::APSInt RInt) { + SValBuilder &SVB = State->getStateManager().getSValBuilder(); + BasicValueFactory &BV = SVB.getBasicValueFactory(); + SymbolManager &SymMgr = SVB.getSymbolManager(); + + QualType SymTy = LSym->getType(); + assert(SymTy == RSym->getType() && + "Symbols are not of the same type!"); + assert(APSIntType(LInt) == BV.getAPSIntType(SymTy) && + "Integers are not of the same type as symbols!"); + assert(APSIntType(RInt) == BV.getAPSIntType(SymTy) && + "Integers are not of the same type as symbols!"); + + QualType ResultTy; + if (BinaryOperator::isComparisonOp(Op)) + ResultTy = SVB.getConditionType(); + else if (BinaryOperator::isAdditiveOp(Op)) + ResultTy = SymTy; + else + llvm_unreachable("Operation not suitable for unchecked rearrangement!"); + + // FIXME: Can we use assume() without getting into an infinite recursion? + if (LSym == RSym) + return SVB.evalBinOpNN(State, Op, nonloc::ConcreteInt(LInt), + nonloc::ConcreteInt(RInt), ResultTy) + .castAs(); + + SymbolRef ResultSym = nullptr; + BinaryOperator::Opcode ResultOp; + llvm::APSInt ResultInt; + if (BinaryOperator::isComparisonOp(Op)) { + // Prefer comparing to a non-negative number. + // FIXME: Maybe it'd be better to have consistency in + // "$x - $y" vs. "$y - $x" because those are solver's keys. + if (LInt > RInt) { + ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy); + ResultOp = BinaryOperator::reverseComparisonOp(Op); + ResultInt = LInt - RInt; // Opposite order! + } else { + ResultSym = SymMgr.getSymSymExpr(LSym, BO_Sub, RSym, SymTy); + ResultOp = Op; + ResultInt = RInt - LInt; // Opposite order! + } + } else { + ResultSym = SymMgr.getSymSymExpr(LSym, Op, RSym, SymTy); + ResultInt = (Op == BO_Add) ? (LInt + RInt) : (LInt - RInt); + ResultOp = BO_Add; + // Bring back the cosmetic difference. + if (ResultInt < 0) { + ResultInt = -ResultInt; + ResultOp = BO_Sub; + } else if (ResultInt == 0) { + // Shortcut: Simplify "$x + 0" to "$x". + return nonloc::SymbolVal(ResultSym); + } + } + const llvm::APSInt &PersistentResultInt = BV.getValue(ResultInt); + return nonloc::SymbolVal( + SymMgr.getSymIntExpr(ResultSym, ResultOp, PersistentResultInt, ResultTy)); +} + +// Rearrange if symbol type matches the result type and if the operator is a +// comparison operator, both symbol and constant must be within constant +// overflow bounds. +static bool shouldRearrange(ProgramStateRef State, BinaryOperator::Opcode Op, + SymbolRef Sym, llvm::APSInt Int, QualType Ty) { + return Sym->getType() == Ty && + (!BinaryOperator::isComparisonOp(Op) || + (isWithinConstantOverflowBounds(Sym, State) && + isWithinConstantOverflowBounds(Int))); +} + +static Optional tryRearrange(ProgramStateRef State, + BinaryOperator::Opcode Op, NonLoc Lhs, + NonLoc Rhs, QualType ResultTy) { + ProgramStateManager &StateMgr = State->getStateManager(); + SValBuilder &SVB = StateMgr.getSValBuilder(); + + // We expect everything to be of the same type - this type. + QualType SingleTy; + + auto &Opts = + StateMgr.getOwningEngine()->getAnalysisManager().getAnalyzerOptions(); + + SymbolRef LSym = Lhs.getAsSymbol(); + if (!LSym) + return None; + + // Always rearrange additive operations but rearrange comparisons only if + // option is set. + if (BinaryOperator::isComparisonOp(Op) && + Opts.shouldAggressivelySimplifyRelationalComparison()) { + SingleTy = LSym->getType(); + if (ResultTy != SVB.getConditionType()) + return None; + // Initialize SingleTy later with a symbol's type. + } else if (BinaryOperator::isAdditiveOp(Op)) { + SingleTy = ResultTy; + // Substracting unsigned integers is a nightmare. + if (!SingleTy->isSignedIntegerOrEnumerationType()) + return None; + } else { + // Don't rearrange other operations. + return None; + } + + assert(!SingleTy.isNull() && "We should have figured out the type by now!"); + + SymbolRef RSym = Rhs.getAsSymbol(); + if (!RSym || RSym->getType() != SingleTy) + return None; + + BasicValueFactory &BV = State->getBasicVals(); + llvm::APSInt LInt, RInt; + std::tie(LSym, LInt) = decomposeSymbol(LSym, BV); + std::tie(RSym, RInt) = decomposeSymbol(RSym, BV); + if (!shouldRearrange(State, Op, LSym, LInt, SingleTy) || + !shouldRearrange(State, Op, RSym, RInt, SingleTy)) + return None; + + // We know that no overflows can occur anymore. + return doRearrangeUnchecked(State, Op, LSym, LInt, RSym, RInt); +} + SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state, BinaryOperator::Opcode op, NonLoc lhs, NonLoc rhs, @@ -559,6 +747,9 @@ if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs)) return MakeSymIntVal(Sym, op, *RHSValue, resultTy); + if (Optional V = tryRearrange(state, op, lhs, rhs, resultTy)) + return *V; + // Give up -- this is not a symbolic expression we can handle. return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy); } Index: cfe/trunk/test/Analysis/conditional-path-notes.c =================================================================== --- cfe/trunk/test/Analysis/conditional-path-notes.c +++ cfe/trunk/test/Analysis/conditional-path-notes.c @@ -78,6 +78,7 @@ void testNonDiagnosableBranchArithmetic(int a, int b) { if (a - b) { // expected-note@-1 {{Taking true branch}} + // expected-note@-2 {{Assuming the condition is true}} *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}} // expected-note@-1 {{Dereference of null pointer}} } @@ -1573,12 +1574,75 @@ // CHECK-NEXT: end // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: kindevent +// CHECK-NEXT: location +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: ranges +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col11 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: depth0 +// CHECK-NEXT: extended_message +// CHECK-NEXT: Assuming the condition is true +// CHECK-NEXT: message +// CHECK-NEXT: Assuming the condition is true +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: kindcontrol +// CHECK-NEXT: edges +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: start +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line79 +// CHECK-NEXT: col7 +// CHECK-NEXT: file0 +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: end +// CHECK-NEXT: +// CHECK-NEXT: +// CHECK-NEXT: line82 // CHECK-NEXT: col5 // CHECK-NEXT: file0 // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col5 // CHECK-NEXT: file0 // CHECK-NEXT: @@ -1594,12 +1658,12 @@ // CHECK-NEXT: start // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col5 // CHECK-NEXT: file0 // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col5 // CHECK-NEXT: file0 // CHECK-NEXT: @@ -1607,12 +1671,12 @@ // CHECK-NEXT: end // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col24 // CHECK-NEXT: file0 // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col24 // CHECK-NEXT: file0 // CHECK-NEXT: @@ -1624,7 +1688,7 @@ // CHECK-NEXT: kindevent // CHECK-NEXT: location // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col24 // CHECK-NEXT: file0 // CHECK-NEXT: @@ -1632,12 +1696,12 @@ // CHECK-NEXT: // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col5 // CHECK-NEXT: file0 // CHECK-NEXT: // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col26 // CHECK-NEXT: file0 // CHECK-NEXT: @@ -1658,10 +1722,10 @@ // CHECK-NEXT: issue_hash_content_of_line_in_contextf56671e5f67c73abef619b56f7c29fa4 // CHECK-NEXT: issue_context_kindfunction // CHECK-NEXT: issue_contexttestNonDiagnosableBranchArithmetic -// CHECK-NEXT: issue_hash_function_offset3 +// CHECK-NEXT: issue_hash_function_offset4 // CHECK-NEXT: location // CHECK-NEXT: -// CHECK-NEXT: line81 +// CHECK-NEXT: line82 // CHECK-NEXT: col24 // CHECK-NEXT: file0 // CHECK-NEXT: Index: cfe/trunk/test/Analysis/explain-svals.cpp =================================================================== --- cfe/trunk/test/Analysis/explain-svals.cpp +++ cfe/trunk/test/Analysis/explain-svals.cpp @@ -69,7 +69,7 @@ static int stat; clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}} clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}} - clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}} + clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}} clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}} clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}} clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}} Index: cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c =================================================================== --- cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c +++ cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c @@ -0,0 +1,931 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s + +void clang_analyzer_dump(int x); +void clang_analyzer_eval(int x); + +void exit(int); + +#define UINT_MAX (~0U) +#define INT_MAX (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__)) + +int g(); +int f() { + int x = g(); + // Assert that no overflows occur in this test file. + // Assuming that concrete integers are also within that range. + assert(x <= ((int)INT_MAX / 4)); + assert(x >= -((int)INT_MAX / 4)); + return x; +} + +void compare_different_symbol_equal() { + int x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}} +} + +void compare_different_symbol_plus_left_int_equal() { + int x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}} +} + +void compare_different_symbol_minus_left_int_equal() { + int x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}} +} + +void compare_different_symbol_plus_right_int_equal() { + int x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}} +} + +void compare_different_symbol_minus_right_int_equal() { + int x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_equal() { + int x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_equal() { + int x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_equal() { + int x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_equal() { + int x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}} +} + +void compare_same_symbol_equal() { + int x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_int_equal() { + int x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_int_equal() { + int x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_right_int_equal() { + int x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_right_int_equal() { + int x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_plus_right_int_equal() { + int x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_minus_right_int_equal() { + int x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_plus_right_int_equal() { + int x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_minus_right_int_equal() { + int x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_different_symbol_less_or_equal() { + int x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}} +} + +void compare_different_symbol_plus_left_int_less_or_equal() { + int x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}} +} + +void compare_different_symbol_minus_left_int_less_or_equal() { + int x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}} +} + +void compare_different_symbol_plus_right_int_less_or_equal() { + int x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}} +} + +void compare_different_symbol_minus_right_int_less_or_equal() { + int x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_less_or_equal() { + int x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_less_or_equal() { + int x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_less_or_equal() { + int x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_less_or_equal() { + int x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}} +} + +void compare_same_symbol_less_or_equal() { + int x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_int_less_or_equal() { + int x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_int_less_or_equal() { + int x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_right_int_less_or_equal() { + int x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_minus_right_int_less_or_equal() { + int x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_plus_right_int_less_or_equal() { + int x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_minus_right_int_less_or_equal() { + int x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_plus_right_int_less_or_equal() { + int x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_minus_left_minus_right_int_less_or_equal() { + int x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_different_symbol_less() { + int x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}} +} + +void compare_different_symbol_plus_left_int_less() { + int x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}} +} + +void compare_different_symbol_minus_left_int_less() { + int x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}} +} + +void compare_different_symbol_plus_right_int_less() { + int x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}} +} + +void compare_different_symbol_minus_right_int_less() { + int x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_less() { + int x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_less() { + int x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_less() { + int x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_less() { + int x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}} +} + +void compare_same_symbol_less() { + int x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_int_less() { + int x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_int_less() { + int x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_right_int_less() { + int x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_minus_right_int_less() { + int x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_plus_right_int_less() { + int x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_minus_right_int_less() { + int x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_minus_left_plus_right_int_less() { + int x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_minus_left_minus_right_int_less() { + int x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_different_symbol_equal_unsigned() { + unsigned x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}} +} + +void compare_different_symbol_plus_left_int_equal_unsigned() { + unsigned x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}} +} + +void compare_different_symbol_minus_left_int_equal_unsigned() { + unsigned x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}} +} + +void compare_different_symbol_plus_right_int_equal_unsigned() { + unsigned x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}} +} + +void compare_different_symbol_minus_right_int_equal_unsigned() { + unsigned x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() { + unsigned x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() { + unsigned x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() { + unsigned x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() { + unsigned x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}} +} + +void compare_same_symbol_equal_unsigned() { + unsigned x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_int_equal_unsigned() { + unsigned x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_int_equal_unsigned() { + unsigned x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_right_int_equal_unsigned() { + unsigned x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_right_int_equal_unsigned() { + unsigned x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() { + unsigned x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() { + unsigned x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() { + unsigned x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x == y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() { + unsigned x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x == y); + // expected-warning@-1{{TRUE}} +} + +void compare_different_symbol_less_or_equal_unsigned() { + unsigned x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}} +} + +void compare_different_symbol_plus_left_int_less_or_equal_unsigned() { + unsigned x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}} +} + +void compare_different_symbol_minus_left_int_less_or_equal_unsigned() { + unsigned x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}} +} + +void compare_different_symbol_plus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}} +} + +void compare_different_symbol_minus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() { + unsigned x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() { + unsigned x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() { + unsigned x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() { + unsigned x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}} +} + +void compare_same_symbol_less_or_equal_unsigned() { + unsigned x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_int_less_or_equal_unsigned() { + unsigned x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_int_less_or_equal_unsigned() { + unsigned x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x <= y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() { + unsigned x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x <= y); + // expected-warning@-1{{TRUE}} +} + +void compare_different_symbol_less_unsigned() { + unsigned x = f(), y = f(); + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}} +} + +void compare_different_symbol_plus_left_int_less_unsigned() { + unsigned x = f()+1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}} +} + +void compare_different_symbol_minus_left_int_less_unsigned() { + unsigned x = f()-1, y = f(); + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}} +} + +void compare_different_symbol_plus_right_int_less_unsigned() { + unsigned x = f(), y = f()+2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}} +} + +void compare_different_symbol_minus_right_int_less_unsigned() { + unsigned x = f(), y = f()-2; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}} +} + +void compare_different_symbol_plus_left_plus_right_int_less_unsigned() { + unsigned x = f()+2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}} +} + +void compare_different_symbol_plus_left_minus_right_int_less_unsigned() { + unsigned x = f()+2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}} +} + +void compare_different_symbol_minus_left_plus_right_int_less_unsigned() { + unsigned x = f()-2, y = f()+1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}} +} + +void compare_different_symbol_minus_left_minus_right_int_less_unsigned() { + unsigned x = f()-2, y = f()-1; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}} + clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}} +} + +void compare_same_symbol_less_unsigned() { + unsigned x = f(), y = x; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_int_less_unsigned() { + unsigned x = f(), y = x; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_int_less_unsigned() { + unsigned x = f(), y = x; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_right_int_less_unsigned() { + unsigned x = f(), y = x+1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_right_int_less_unsigned() { + unsigned x = f(), y = x-1; + clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_plus_left_plus_right_int_less_unsigned() { + unsigned x = f(), y = x+1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void compare_same_symbol_plus_left_minus_right_int_less_unsigned() { + unsigned x = f(), y = x-1; + ++x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_plus_right_int_less_unsigned() { + unsigned x = f(), y = x+1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}} + clang_analyzer_dump(x < y); + // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified? +} + +void compare_same_symbol_minus_left_minus_right_int_less_unsigned() { + unsigned x = f(), y = x-1; + --x; + clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}} + clang_analyzer_eval(x < y); + // expected-warning@-1{{FALSE}} +} + +void overflow(signed char n, signed char m) { + if (n + 0 > m + 0) { + clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}} + } +}