//===----------------------------------------------------------------------===//
#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;
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<DefinedSVal>()) {
+ 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<SymbolRef, llvm::APSInt>
+decomposeSymbol(SymbolRef Sym, BasicValueFactory &BV) {
+ if (const auto *SymInt = dyn_cast<SymIntExpr>(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<NonLoc>();
+
+ 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<NonLoc> 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,
if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
+ if (Optional<NonLoc> 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);
}
--- /dev/null
+// 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}}
+ }
+}