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

Artem Dergachev via cfe-commits cfe-commits at lists.llvm.org
Mon Apr 16 18:33:40 PDT 2018


That's a combination of the simplifySVal() mechanism and the new 
rearrangement mechanism that causes the regression. I guess that's where 
we get when we try to squeeze more stuff into our solver. It seems safe 
to reduce simplifySVal() complexity threshold to 10 or 20 but i'm also 
curious whether something could be fixed in the rearrangement algorithm 
(probably it also needs a threshold?). I'll see what i can do, but i'll 
be relatively busy this week.

On 4/16/18 5:39 AM, Mikael Holmén wrote:
> 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
>>



More information about the cfe-commits mailing list