r329780 - [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

Mikael Holmén via cfe-commits cfe-commits at lists.llvm.org
Mon Apr 16 05:39:26 PDT 2018


Hi Adam and Artem,

If I run

clang-tidy -header-filter=.\* 
-checks=clang-analyzer-\*,-clang-analyzer-unix\*,-clang-analyzer-osx\*,-clang-analyzer-security\*,-clang-analyzer-valist\*,-clang-analyzer-optin\*,-clang-analyzer-nullability\*,-clang-analyzer-llvm.Conventions,-clang-analyzer-deadcode.DeadStores,-clang-analyzer-cplusplus\*,-clang-analyzer-apiModeling\* 
test.c --

on the attached test.c it takes seemingly forever, but if I peel off a 
number of calls to "f" it starts terminating.

It seems like every additional level of calls to "f" doubles the 
compilation time with your commit.

Without your commit even the full repriducer terminates quickly.

Regards,
Mikael

On 04/11/2018 08:21 AM, Adam Balogh via cfe-commits wrote:
> Author: baloghadamsoftware
> Date: Tue Apr 10 23:21:12 2018
> New Revision: 329780
> 
> URL: http://llvm.org/viewvc/llvm-project?rev=329780&view=rev
> Log:
> [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)
> 
> Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. A + n >= B + m becomes A - B >= m - n which enables the constraint manager to store a range m - n .. MAX_VALUE for the symbolic expression A - B. This can be used later to check whether e.g. A + k == B + l can be true, which is also rearranged to A - B == l - k so the constraint manager can check whether l - k is in the range (thus greater than or equal to m - n).
> 
> The restriction in this version is the the rearrangement happens only if both the symbols and the concrete integers are within the range [min/4 .. max/4] where min and max are the minimal and maximal values of their type.
> 
> The rearrangement is not enabled by default. It has to be enabled by using -analyzer-config aggressive-relational-comparison-simplification=true.
> 
> Co-author of this patch is Artem Dergachev (NoQ).
> 
> Differential Revision: https://reviews.llvm.org/D41938
> 
> 
> Added:
>      cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
> Modified:
>      cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
>      cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
>      cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
>      cfe/trunk/test/Analysis/conditional-path-notes.c
>      cfe/trunk/test/Analysis/explain-svals.cpp
> 
> Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=329780&r1=329779&r2=329780&view=diff
> ==============================================================================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Tue Apr 10 23:21:12 2018
> @@ -312,6 +312,9 @@ private:
>     /// \sa shouldDisplayNotesAsEvents
>     Optional<bool> DisplayNotesAsEvents;
>   
> +  /// \sa shouldAggressivelySimplifyRelationalComparison
> +  Optional<bool> AggressiveRelationalComparisonSimplification;
> +
>     /// \sa getCTUDir
>     Optional<StringRef> CTUDir;
>   
> @@ -666,6 +669,20 @@ public:
>     /// 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 <REL> B + m becomes A - B <REL> m - n, where A and B symbolic,
> +  /// n and m are integers. <REL> 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();
>   
> 
> Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=329780&r1=329779&r2=329780&view=diff
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Tue Apr 10 23:21:12 2018
> @@ -445,6 +445,14 @@ bool AnalyzerOptions::shouldDisplayNotes
>     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", "");
> 
> Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp?rev=329780&r1=329779&r2=329780&view=diff
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp Tue Apr 10 23:21:12 2018
> @@ -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 @@ SVal SimpleSValBuilder::MakeSymIntVal(co
>     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,
> @@ -559,6 +747,9 @@ SVal SimpleSValBuilder::evalBinOpNN(Prog
>         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);
>       }
> 
> Modified: cfe/trunk/test/Analysis/conditional-path-notes.c
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/conditional-path-notes.c?rev=329780&r1=329779&r2=329780&view=diff
> ==============================================================================
> --- cfe/trunk/test/Analysis/conditional-path-notes.c (original)
> +++ cfe/trunk/test/Analysis/conditional-path-notes.c Tue Apr 10 23:21:12 2018
> @@ -78,6 +78,7 @@ void testDiagnosableBranchLogical(int a,
>   void testNonDiagnosableBranchArithmetic(int a, int b) {
>     if (a - b) {
>       // expected-note at -1 {{Taking true branch}}
> +    // expected-note at -2 {{Assuming the condition is true}}
>       *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
>       // expected-note at -1 {{Dereference of null pointer}}
>     }
> @@ -1573,12 +1574,75 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:         <key>end</key>
>   // CHECK-NEXT:          <array>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>79</integer>
> +// CHECK-NEXT:            <key>col</key><integer>7</integer>
> +// CHECK-NEXT:            <key>file</key><integer>0</integer>
> +// CHECK-NEXT:           </dict>
> +// CHECK-NEXT:           <dict>
> +// CHECK-NEXT:            <key>line</key><integer>79</integer>
> +// CHECK-NEXT:            <key>col</key><integer>7</integer>
> +// CHECK-NEXT:            <key>file</key><integer>0</integer>
> +// CHECK-NEXT:           </dict>
> +// CHECK-NEXT:          </array>
> +// CHECK-NEXT:        </dict>
> +// CHECK-NEXT:       </array>
> +// CHECK-NEXT:     </dict>
> +// CHECK-NEXT:     <dict>
> +// CHECK-NEXT:      <key>kind</key><string>event</string>
> +// CHECK-NEXT:      <key>location</key>
> +// CHECK-NEXT:      <dict>
> +// CHECK-NEXT:       <key>line</key><integer>79</integer>
> +// CHECK-NEXT:       <key>col</key><integer>7</integer>
> +// CHECK-NEXT:       <key>file</key><integer>0</integer>
> +// CHECK-NEXT:      </dict>
> +// CHECK-NEXT:      <key>ranges</key>
> +// CHECK-NEXT:      <array>
> +// CHECK-NEXT:        <array>
> +// CHECK-NEXT:         <dict>
> +// CHECK-NEXT:          <key>line</key><integer>79</integer>
> +// CHECK-NEXT:          <key>col</key><integer>7</integer>
> +// CHECK-NEXT:          <key>file</key><integer>0</integer>
> +// CHECK-NEXT:         </dict>
> +// CHECK-NEXT:         <dict>
> +// CHECK-NEXT:          <key>line</key><integer>79</integer>
> +// CHECK-NEXT:          <key>col</key><integer>11</integer>
> +// CHECK-NEXT:          <key>file</key><integer>0</integer>
> +// CHECK-NEXT:         </dict>
> +// CHECK-NEXT:        </array>
> +// CHECK-NEXT:      </array>
> +// CHECK-NEXT:      <key>depth</key><integer>0</integer>
> +// CHECK-NEXT:      <key>extended_message</key>
> +// CHECK-NEXT:      <string>Assuming the condition is true</string>
> +// CHECK-NEXT:      <key>message</key>
> +// CHECK-NEXT:      <string>Assuming the condition is true</string>
> +// CHECK-NEXT:     </dict>
> +// CHECK-NEXT:     <dict>
> +// CHECK-NEXT:      <key>kind</key><string>control</string>
> +// CHECK-NEXT:      <key>edges</key>
> +// CHECK-NEXT:       <array>
> +// CHECK-NEXT:        <dict>
> +// CHECK-NEXT:         <key>start</key>
> +// CHECK-NEXT:          <array>
> +// CHECK-NEXT:           <dict>
> +// CHECK-NEXT:            <key>line</key><integer>79</integer>
> +// CHECK-NEXT:            <key>col</key><integer>7</integer>
> +// CHECK-NEXT:            <key>file</key><integer>0</integer>
> +// CHECK-NEXT:           </dict>
> +// CHECK-NEXT:           <dict>
> +// CHECK-NEXT:            <key>line</key><integer>79</integer>
> +// CHECK-NEXT:            <key>col</key><integer>7</integer>
> +// CHECK-NEXT:            <key>file</key><integer>0</integer>
> +// CHECK-NEXT:           </dict>
> +// CHECK-NEXT:          </array>
> +// CHECK-NEXT:         <key>end</key>
> +// CHECK-NEXT:          <array>
> +// CHECK-NEXT:           <dict>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>5</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>5</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
> @@ -1594,12 +1658,12 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:         <key>start</key>
>   // CHECK-NEXT:          <array>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>5</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>5</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
> @@ -1607,12 +1671,12 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:         <key>end</key>
>   // CHECK-NEXT:          <array>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>24</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
>   // CHECK-NEXT:           <dict>
> -// CHECK-NEXT:            <key>line</key><integer>81</integer>
> +// CHECK-NEXT:            <key>line</key><integer>82</integer>
>   // CHECK-NEXT:            <key>col</key><integer>24</integer>
>   // CHECK-NEXT:            <key>file</key><integer>0</integer>
>   // CHECK-NEXT:           </dict>
> @@ -1624,7 +1688,7 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:      <key>kind</key><string>event</string>
>   // CHECK-NEXT:      <key>location</key>
>   // CHECK-NEXT:      <dict>
> -// CHECK-NEXT:       <key>line</key><integer>81</integer>
> +// CHECK-NEXT:       <key>line</key><integer>82</integer>
>   // CHECK-NEXT:       <key>col</key><integer>24</integer>
>   // CHECK-NEXT:       <key>file</key><integer>0</integer>
>   // CHECK-NEXT:      </dict>
> @@ -1632,12 +1696,12 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:      <array>
>   // CHECK-NEXT:        <array>
>   // CHECK-NEXT:         <dict>
> -// CHECK-NEXT:          <key>line</key><integer>81</integer>
> +// CHECK-NEXT:          <key>line</key><integer>82</integer>
>   // CHECK-NEXT:          <key>col</key><integer>5</integer>
>   // CHECK-NEXT:          <key>file</key><integer>0</integer>
>   // CHECK-NEXT:         </dict>
>   // CHECK-NEXT:         <dict>
> -// CHECK-NEXT:          <key>line</key><integer>81</integer>
> +// CHECK-NEXT:          <key>line</key><integer>82</integer>
>   // CHECK-NEXT:          <key>col</key><integer>26</integer>
>   // CHECK-NEXT:          <key>file</key><integer>0</integer>
>   // CHECK-NEXT:         </dict>
> @@ -1658,10 +1722,10 @@ void testNonDiagnosableBranchArithmetic(
>   // CHECK-NEXT:    <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
>   // CHECK-NEXT:   <key>issue_context_kind</key><string>function</string>
>   // CHECK-NEXT:   <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
> -// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>3</string>
> +// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>4</string>
>   // CHECK-NEXT:   <key>location</key>
>   // CHECK-NEXT:   <dict>
> -// CHECK-NEXT:    <key>line</key><integer>81</integer>
> +// CHECK-NEXT:    <key>line</key><integer>82</integer>
>   // CHECK-NEXT:    <key>col</key><integer>24</integer>
>   // CHECK-NEXT:    <key>file</key><integer>0</integer>
>   // CHECK-NEXT:   </dict>
> 
> Modified: cfe/trunk/test/Analysis/explain-svals.cpp
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/explain-svals.cpp?rev=329780&r1=329779&r2=329780&view=diff
> ==============================================================================
> --- cfe/trunk/test/Analysis/explain-svals.cpp (original)
> +++ cfe/trunk/test/Analysis/explain-svals.cpp Tue Apr 10 23:21:12 2018
> @@ -69,7 +69,7 @@ void test_4(int x, int y) {
>     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'$}}}}
> 
> Added: cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c?rev=329780&view=auto
> ==============================================================================
> --- cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c (added)
> +++ cfe/trunk/test/Analysis/svalbuilder-rearrange-comparisons.c Tue Apr 10 23:21:12 2018
> @@ -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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 at -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}}
> +  }
> +}
> 
> 
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: text/x-csrc
Size: 407 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180416/ed70d711/attachment-0001.c>


More information about the cfe-commits mailing list