[analyzer] Rework both constraint managers to handle mixed-type comparisons.

This involves keeping track of three separate types: the symbol type, the
adjustment type, and the comparison type. For example, in "$x + 5 > 0ULL",
if the type of $x is 'signed char', the adjustment type is 'int' and the
comparison type is 'unsigned long long'. Most of the time these three types
will be the same, but we should still do the right thing when the
comparison value is out of range, and wraparound should be calculated in
the adjustment type.

This also re-disables an out-of-bounds test; we were extracting the symbol
from non-additive SymIntExprs, but then throwing away the integer.

Sorry for the large patch; both the basic and range constraint managers needed
to be updated together, since they share code in SimpleConstraintManager.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@156361 91177308-0d34-0410-b5e6-96231b3b80d8
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
index dcb7779..e1ff17b 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
@@ -51,6 +51,11 @@
     return Result;
   }
 
+  /// Returns an all-zero value for this type.
+  llvm::APSInt getZeroValue() const LLVM_READONLY {
+    return llvm::APSInt(BitWidth, IsUnsigned);
+  }
+
   /// Returns the minimum value for this type.
   llvm::APSInt getMinValue() const LLVM_READONLY {
     return llvm::APSInt::getMinValue(BitWidth, IsUnsigned);
@@ -61,6 +66,21 @@
     return llvm::APSInt::getMaxValue(BitWidth, IsUnsigned);
   }
 
+  /// Used to classify whether a value is representable using this type.
+  ///
+  /// \see testInRange
+  enum RangeTestResultKind {
+    RTR_Below = -1, ///< Value is less than the minimum representable value.
+    RTR_Within = 0, ///< Value is representable using this type.
+    RTR_Above = 1   ///< Value is greater than the maximum representable value.
+  };
+
+  /// Tests whether a given value is losslessly representable using this type.
+  ///
+  /// Note that signedness conversions will be rejected, even with the same bit
+  /// pattern. For example, -1s8 is not in range for 'unsigned char' (u8).
+  RangeTestResultKind testInRange(const llvm::APSInt &Val) const LLVM_READONLY;
+  
   bool operator==(const APSIntType &Other) const {
     return BitWidth == Other.BitWidth && IsUnsigned == Other.IsUnsigned;
   }
diff --git a/lib/StaticAnalyzer/Core/APSIntType.cpp b/lib/StaticAnalyzer/Core/APSIntType.cpp
new file mode 100644
index 0000000..884b0fa
--- /dev/null
+++ b/lib/StaticAnalyzer/Core/APSIntType.cpp
@@ -0,0 +1,38 @@
+//===--- APSIntType.cpp - Simple record of the type of APSInts ------------===//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+
+using namespace clang;
+using namespace ento;
+
+APSIntType::RangeTestResultKind
+APSIntType::testInRange(const llvm::APSInt &Value) const {
+  // Negative numbers cannot be losslessly converted to unsigned type.
+  if (IsUnsigned && Value.isSigned() && Value.isNegative())
+    return RTR_Below;
+
+  // Signed integers can be converted to signed integers of the same width
+  // or (if positive) unsigned integers with one fewer bit.
+  // Unsigned integers can be converted to unsigned integers of the same width
+  // or signed integers with one more bit.
+  unsigned MinBits;
+  if (Value.isSigned())
+    MinBits = Value.getMinSignedBits() - IsUnsigned;
+  else
+    MinBits = Value.getActiveBits() + !IsUnsigned;
+
+  if (MinBits <= BitWidth)
+    return RTR_Within;
+
+  if (Value.isSigned() && Value.isNegative())
+    return RTR_Below;
+  else
+    return RTR_Above;
+}
diff --git a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp b/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
index 2d9addd..7a095d5 100644
--- a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "llvm/Support/raw_ostream.h"
@@ -53,18 +54,25 @@
   ProgramState::IntSetTy::Factory ISetFactory;
 public:
   BasicConstraintManager(ProgramStateManager &statemgr, SubEngine &subengine)
-    : SimpleConstraintManager(subengine), 
+    : SimpleConstraintManager(subengine, statemgr.getBasicVals()),
       ISetFactory(statemgr.getAllocator()) {}
 
-  ProgramStateRef assumeSymNE(ProgramStateRef state,
-                                  SymbolRef sym,
-                                  const llvm::APSInt& V,
-                                  const llvm::APSInt& Adjustment);
+  ProgramStateRef assumeSymEquality(ProgramStateRef State, SymbolRef Sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment,
+                                    bool Assumption);
 
-  ProgramStateRef assumeSymEQ(ProgramStateRef state,
-                                  SymbolRef sym,
-                                  const llvm::APSInt& V,
-                                  const llvm::APSInt& Adjustment);
+  ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) {
+    return assumeSymEquality(State, Sym, V, Adjustment, false);
+  }
+
+  ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) {
+    return assumeSymEquality(State, Sym, V, Adjustment, true);
+  }
 
   ProgramStateRef assumeSymLT(ProgramStateRef state,
                                   SymbolRef sym,
@@ -108,6 +116,9 @@
   ProgramStateRef removeDeadBindings(ProgramStateRef state,
                                          SymbolReaper& SymReaper);
 
+  bool performTest(llvm::APSInt SymVal, llvm::APSInt Adjustment,
+                   BinaryOperator::Opcode Op, llvm::APSInt ComparisonVal);
+
   void print(ProgramStateRef state,
              raw_ostream &Out,
              const char* nl,
@@ -122,60 +133,94 @@
   return new BasicConstraintManager(statemgr, subengine);
 }
 
-ProgramStateRef 
-BasicConstraintManager::assumeSymNE(ProgramStateRef state,
-                                    SymbolRef sym,
-                                    const llvm::APSInt &V,
-                                    const llvm::APSInt &Adjustment) {
-  // First, determine if sym == X, where X+Adjustment != V.
-  llvm::APSInt Adjusted = V-Adjustment;
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X != Adjusted);
-    return isFeasible ? state : NULL;
-  }
+// FIXME: This is a more general utility and should live somewhere else.
+bool BasicConstraintManager::performTest(llvm::APSInt SymVal,
+                                         llvm::APSInt Adjustment,
+                                         BinaryOperator::Opcode Op,
+                                         llvm::APSInt ComparisonVal) {
+  APSIntType Type(Adjustment);
+  Type.apply(SymVal);
+  Type.apply(ComparisonVal);
+  SymVal += Adjustment;
 
-  // Second, determine if sym+Adjustment != V.
-  if (isNotEqual(state, sym, Adjusted))
-    return state;
+  assert(BinaryOperator::isComparisonOp(Op));
+  BasicValueFactory &BVF = getBasicVals();
+  const llvm::APSInt *Result = BVF.evalAPSInt(Op, SymVal, ComparisonVal);
+  assert(Result && "Comparisons should always have valid results.");
 
-  // If we reach here, sym is not a constant and we don't know if it is != V.
-  // Make that assumption.
-  return AddNE(state, sym, Adjusted);
+  return Result->getBoolValue();
 }
 
-ProgramStateRef 
-BasicConstraintManager::assumeSymEQ(ProgramStateRef state,
-                                    SymbolRef sym,
-                                    const llvm::APSInt &V,
-                                    const llvm::APSInt &Adjustment) {
-  // First, determine if sym == X, where X+Adjustment != V.
-  llvm::APSInt Adjusted = V-Adjustment;
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X == Adjusted);
-    return isFeasible ? state : NULL;
+ProgramStateRef
+BasicConstraintManager::assumeSymEquality(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &V,
+                                          const llvm::APSInt &Adjustment,
+                                          bool Assumption) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  if (AdjustmentType.testInRange(V) != APSIntType::RTR_Within)
+    return Assumption ? NULL : State;
+
+  // Get the symbol type.
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
+  APSIntType SymbolType = BVF.getAPSIntType(Sym->getType(Ctx));
+
+  // First, see if the adjusted value is within range for the symbol.
+  llvm::APSInt Adjusted = AdjustmentType.convert(V) - Adjustment;
+  if (SymbolType.testInRange(Adjusted) != APSIntType::RTR_Within)
+    return Assumption ? NULL : State;
+
+  // Now we can do things properly in the symbol space.
+  SymbolType.apply(Adjusted);
+
+  // Second, determine if sym == X, where X+Adjustment != V.
+  if (const llvm::APSInt *X = getSymVal(State, Sym)) {
+    bool IsFeasible = (*X == Adjusted);
+    return (IsFeasible == Assumption) ? State : NULL;
   }
 
-  // Second, determine if sym+Adjustment != V.
-  if (isNotEqual(state, sym, Adjusted))
-    return NULL;
+  // Third, determine if we already know sym+Adjustment != V.
+  if (isNotEqual(State, Sym, Adjusted))
+    return Assumption ? NULL : State;
 
-  // If we reach here, sym is not a constant and we don't know if it is == V.
-  // Make that assumption.
-  return AddEQ(state, sym, Adjusted);
+  // If we reach here, sym is not a constant and we don't know if it is != V.
+  // Make the correct assumption.
+  if (Assumption)
+    return AddEQ(State, Sym, Adjusted);
+  else
+    return AddNE(State, Sym, Adjusted);
 }
 
 // The logic for these will be handled in another ConstraintManager.
+// Approximate it here anyway by handling some edge cases.
 ProgramStateRef 
 BasicConstraintManager::assumeSymLT(ProgramStateRef state,
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Is 'V' the smallest possible value?
-  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
+
+  // Is 'V' out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V > ComparisonType.convert(Max)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Is 'V' the smallest possible value, or out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V <= ComparisonType.convert(Min)) {
     // sym cannot be any value less than 'V'.  This path is infeasible.
     return NULL;
   }
 
+  // Reject a path if the value of sym is a constant X and !(X+Adj < V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_LT, V);
+    return isFeasible ? state : NULL;
+  }
+
   // FIXME: For now have assuming x < y be the same as assuming sym != V;
   return assumeSymNE(state, sym, V, Adjustment);
 }
@@ -185,12 +230,28 @@
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Is 'V' the largest possible value?
-  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
+
+  // Is 'V' the largest possible value, or out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V >= ComparisonType.convert(Max)) {
     // sym cannot be any value greater than 'V'.  This path is infeasible.
     return NULL;
   }
 
+  // Is 'V' out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V < ComparisonType.convert(Min)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj > V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_GT, V);
+    return isFeasible ? state : NULL;
+  }
+
   // FIXME: For now have assuming x > y be the same as assuming sym != V;
   return assumeSymNE(state, sym, V, Adjustment);
 }
@@ -200,25 +261,33 @@
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
-  if (const llvm::APSInt *X = getSymVal(state, sym)) {
-    bool isFeasible = (*X >= V-Adjustment);
-    return isFeasible ? state : NULL;
-  }
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
 
-  // Sym is not a constant, but it is worth looking to see if V is the
-  // maximum integer value.
-  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
-    llvm::APSInt Adjusted = V-Adjustment;
+  // Is 'V' the largest possible value, or out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  ComparisonType.apply(Max);
 
-    // If we know that sym != V (after adjustment), then this condition
-    // is infeasible since there is no other value greater than V.
-    bool isFeasible = !isNotEqual(state, sym, Adjusted);
-
-    // If the path is still feasible then as a consequence we know that
+  if (V > Max) {
+    // sym cannot be any value greater than 'V'.  This path is infeasible.
+    return NULL;
+  } else if (V == Max) {
+    // If the path is feasible then as a consequence we know that
     // 'sym+Adjustment == V' because there are no larger values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
+    return assumeSymEQ(state, sym, V, Adjustment);
+  }
+
+  // Is 'V' out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V < ComparisonType.convert(Min)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_GE, V);
+    return isFeasible ? state : NULL;
   }
 
   return state;
@@ -229,25 +298,33 @@
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X <= V-Adjustment);
-    return isFeasible ? state : NULL;
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
+
+  // Is 'V' out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V > ComparisonType.convert(Max)) {
+    // This path is trivially feasible.
+    return state;
   }
 
-  // Sym is not a constant, but it is worth looking to see if V is the
-  // minimum integer value.
-  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
-    llvm::APSInt Adjusted = V-Adjustment;
+  // Is 'V' the smallest possible value, or out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  ComparisonType.apply(Min);
 
-    // If we know that sym != V (after adjustment), then this condition
-    // is infeasible since there is no other value less than V.
-    bool isFeasible = !isNotEqual(state, sym, Adjusted);
-
-    // If the path is still feasible then as a consequence we know that
+  if (V < Min) {
+    // sym cannot be any value less than 'V'.  This path is infeasible.
+    return NULL;
+  } else if (V == Min) {
+    // If the path is feasible then as a consequence we know that
     // 'sym+Adjustment == V' because there are no smaller values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
+    return assumeSymEQ(state, sym, V, Adjustment);
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_LE, V);
+    return isFeasible ? state : NULL;
   }
 
   return state;
@@ -257,7 +334,7 @@
                                                   SymbolRef sym,
                                              const llvm::APSInt& V) {
   // Create a new state with the old binding replaced.
-  return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V));
+  return state->set<ConstEq>(sym, &getBasicVals().getValue(V));
 }
 
 ProgramStateRef BasicConstraintManager::AddNE(ProgramStateRef state,
@@ -269,7 +346,7 @@
   ProgramState::IntSetTy S = T ? *T : ISetFactory.getEmptySet();
 
   // Now add V to the NE set.
-  S = ISetFactory.add(S, &state->getBasicVals().getValue(V));
+  S = ISetFactory.add(S, &getBasicVals().getValue(V));
 
   // Create a new state with the old binding replaced.
   return state->set<ConstNotEq>(sym, S);
@@ -289,7 +366,7 @@
   const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
 
   // See if V is present in the NE-set.
-  return T ? T->contains(&state->getBasicVals().getValue(V)) : false;
+  return T ? T->contains(&getBasicVals().getValue(V)) : false;
 }
 
 bool BasicConstraintManager::isEqual(ProgramStateRef state,
diff --git a/lib/StaticAnalyzer/Core/CMakeLists.txt b/lib/StaticAnalyzer/Core/CMakeLists.txt
index 1ea25bd..23d1dcc 100644
--- a/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -4,6 +4,7 @@
 
 add_clang_library(clangStaticAnalyzerCore
   AnalysisManager.cpp
+  APSIntType.cpp
   BasicConstraintManager.cpp
   BasicValueFactory.cpp
   BlockCounter.cpp
diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 98eb958..550404a 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "llvm/Support/Debug.h"
@@ -143,6 +144,92 @@
     }
   }
 
+  const llvm::APSInt &getMinValue() const {
+    assert(!isEmpty());
+    return ranges.begin()->From();
+  }
+
+  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
+    // This function has nine cases, the cartesian product of range-testing
+    // both the upper and lower bounds against the symbol's type.
+    // Each case requires a different pinning operation.
+    // The function returns false if the described range is entirely outside
+    // the range of values for the associated symbol.
+    APSIntType Type(getMinValue());
+    APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower);
+    APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper);
+
+    switch (LowerTest) {
+    case APSIntType::RTR_Below:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The entire range is outside the symbol's set of possible values.
+        // If this is a conventionally-ordered range, the state is infeasible.
+        if (Lower < Upper)
+          return false;
+
+        // However, if the range wraps around, it spans all possible values.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      case APSIntType::RTR_Within:
+        // The range starts below what's possible but ends within it. Pin.
+        Lower = Type.getMinValue();
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The range spans all possible values for the symbol. Pin.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    case APSIntType::RTR_Within:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The range wraps around, but all lower values are not possible.
+        Type.apply(Lower);
+        Upper = Type.getMaxValue();
+        break;
+      case APSIntType::RTR_Within:
+        // The range may or may not wrap around, but both limits are valid.
+        Type.apply(Lower);
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The range starts within what's possible but ends above it. Pin.
+        Type.apply(Lower);
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    case APSIntType::RTR_Above:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The range wraps but is outside the symbol's set of possible values.
+        return false;
+      case APSIntType::RTR_Within:
+        // The range starts above what's possible but ends within it (wrap).
+        Lower = Type.getMinValue();
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The entire range is outside the symbol's set of possible values.
+        // If this is a conventionally-ordered range, the state is infeasible.
+        if (Lower < Upper)
+          return false;
+
+        // However, if the range wraps around, it spans all possible values.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    }
+
+    return true;
+  }
+
 public:
   // Returns a set containing the values in the receiving set, intersected with
   // the closed range [Lower, Upper]. Unlike the Range type, this range uses
@@ -152,8 +239,10 @@
   // intersection with the two ranges [Min, Upper] and [Lower, Max],
   // or, alternatively, /removing/ all integers between Upper and Lower.
   RangeSet Intersect(BasicValueFactory &BV, Factory &F,
-                     const llvm::APSInt &Lower,
-                     const llvm::APSInt &Upper) const {
+                     llvm::APSInt Lower, llvm::APSInt Upper) const {
+    if (!pin(Lower, Upper))
+      return F.getEmptySet();
+
     PrimRangeSet newRanges = F.getEmptySet();
 
     PrimRangeSet::iterator i = begin(), e = end();
@@ -166,6 +255,7 @@
       IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
       IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
     }
+
     return newRanges;
   }
 
@@ -206,8 +296,8 @@
 class RangeConstraintManager : public SimpleConstraintManager{
   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
 public:
-  RangeConstraintManager(SubEngine &subengine)
-    : SimpleConstraintManager(subengine) {}
+  RangeConstraintManager(SubEngine &subengine, BasicValueFactory &BVF)
+    : SimpleConstraintManager(subengine, BVF) {}
 
   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
                              const llvm::APSInt& Int,
@@ -252,9 +342,9 @@
 
 } // end anonymous namespace
 
-ConstraintManager* ento::CreateRangeConstraintManager(ProgramStateManager&,
-                                                    SubEngine &subeng) {
-  return new RangeConstraintManager(subeng);
+ConstraintManager *
+ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine &Eng) {
+  return new RangeConstraintManager(Eng, StMgr.getBasicVals());
 }
 
 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
@@ -288,8 +378,8 @@
 
   // Lazily generate a new RangeSet representing all possible values for the
   // given symbol type.
-  QualType T = state->getSymbolManager().getType(sym);
-  BasicValueFactory& BV = state->getBasicVals();
+  BasicValueFactory &BV = getBasicVals();
+  QualType T = sym->getType(BV.getContext());
   return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
 }
 
@@ -306,117 +396,154 @@
 // UINT_MAX, 0, 1, and 2.
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
+RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
+    return St;
 
-  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
   llvm::APSInt Upper = Lower;
   --Lower;
   ++Upper;
 
   // [Int-Adjustment+1, Int-Adjustment-1]
   // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
+RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
+    return NULL;
+
   // [Int-Adjustment, Int-Adjustment]
-  BasicValueFactory &BV = state->getBasicVals();
-  llvm::APSInt AdjInt = Int-Adjustment;
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Min = BV.getMinValue(T);
+RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  switch (AdjustmentType.testInRange(Int)) {
+  case APSIntType::RTR_Below:
+    return NULL;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return St;
+  }
 
   // Special case for Int == Min. This is always false.
-  if (Int == Min)
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (ComparisonVal == Min)
     return NULL;
 
   llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = Int-Adjustment;
+  llvm::APSInt Upper = ComparisonVal-Adjustment;
   --Upper;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Max = BV.getMaxValue(T);
+RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  switch (AdjustmentType.testInRange(Int)) {
+  case APSIntType::RTR_Below:
+    return St;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return NULL;
+  }
 
   // Special case for Int == Max. This is always false.
-  if (Int == Max)
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (ComparisonVal == Max)
     return NULL;
 
-  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Lower = ComparisonVal-Adjustment;
   llvm::APSInt Upper = Max-Adjustment;
   ++Lower;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Min = BV.getMinValue(T);
+RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  switch (AdjustmentType.testInRange(Int)) {
+  case APSIntType::RTR_Below:
+    return St;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return NULL;
+  }
 
   // Special case for Int == Min. This is always feasible.
-  if (Int == Min)
-    return state;
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (ComparisonVal == Min)
+    return St;
 
-  const llvm::APSInt &Max = BV.getMaxValue(T);
-
-  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  llvm::APSInt Lower = ComparisonVal-Adjustment;
   llvm::APSInt Upper = Max-Adjustment;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Max = BV.getMaxValue(T);
+RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  switch (AdjustmentType.testInRange(Int)) {
+  case APSIntType::RTR_Below:
+    return NULL;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return St;
+  }
 
   // Special case for Int == Max. This is always feasible.
-  if (Int == Max)
-    return state;
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (ComparisonVal == Max)
+    return St;
 
-  const llvm::APSInt &Min = BV.getMinValue(T);
-
+  llvm::APSInt Min = AdjustmentType.getMinValue();
   llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = Int-Adjustment;
+  llvm::APSInt Upper = ComparisonVal-Adjustment;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 //===------------------------------------------------------------------------===
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index a76a2da..92a8eb1 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 
@@ -71,9 +72,6 @@
 
 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
                                                   Loc Cond, bool Assumption) {
-
-  BasicValueFactory &BasicVals = state->getBasicVals();
-
   switch (Cond.getSubKind()) {
   default:
     assert (false && "'Assume' not implemented for this Loc.");
@@ -88,7 +86,7 @@
     while (SubR) {
       // FIXME: now we only find the first symbolic region.
       if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
-        const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
+        const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
         if (Assumption)
           return assumeSymNE(state, SymR->getSymbol(), zero, zero);
         else
@@ -134,12 +132,12 @@
 }
 
 
-ProgramStateRef SimpleConstraintManager::assumeAuxForSymbol(
-                                              ProgramStateRef State,
-                                              SymbolRef Sym,
-                                              bool Assumption) {
-  QualType T =  State->getSymbolManager().getType(Sym);
-  const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
+ProgramStateRef
+SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
+                                            SymbolRef Sym, bool Assumption) {
+  BasicValueFactory &BVF = getBasicVals();
+  QualType T = Sym->getType(BVF.getContext());
+  const llvm::APSInt &zero = BVF.getValue(0, T);
   if (Assumption)
     return assumeSymNE(State, Sym, zero, zero);
   else
@@ -158,8 +156,7 @@
     return assumeAuxForSymbol(state, sym, Assumption);
   }
 
-  BasicValueFactory &BasicVals = state->getBasicVals();
-  SymbolManager &SymMgr = state->getSymbolManager();
+  BasicValueFactory &BasicVals = getBasicVals();
 
   switch (Cond.getSubKind()) {
   default:
@@ -184,7 +181,7 @@
       BinaryOperator::Opcode op = SE->getOpcode();
       // Implicitly compare non-comparison expressions to 0.
       if (!BinaryOperator::isComparisonOp(op)) {
-        QualType T = SymMgr.getType(SE);
+        QualType T = SE->getType(BasicVals.getContext());
         const llvm::APSInt &zero = BasicVals.getValue(0, T);
         op = (Assumption ? BO_NE : BO_EQ);
         return assumeSymRel(state, SE, op, zero);
@@ -209,33 +206,20 @@
   } // end switch
 }
 
-static llvm::APSInt computeAdjustment(const SymExpr *LHS,
-                                      SymbolRef &Sym) {
-  llvm::APSInt DefaultAdjustment;
-  DefaultAdjustment = 0;
+static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
+  // Is it a "($sym+constant1)" expression?
+  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SE->getOpcode();
+    if (Op == BO_Add || Op == BO_Sub) {
+      Sym = SE->getLHS();
+      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
 
-  // First check if the LHS is a simple symbol reference.
-  if (isa<SymbolData>(LHS))
-    return DefaultAdjustment;
-
-  // Next, see if it's a "($sym+constant1)" expression.
-  const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
-
-  // We cannot simplify "($sym1+$sym2)".
-  if (!SE)
-    return DefaultAdjustment;
-
-  // Get the constant out of the expression "($sym+constant1)" or
-  // "<expr>+constant1".
-  Sym = SE->getLHS();
-  switch (SE->getOpcode()) {
-  case BO_Add:
-    return SE->getRHS();
-  case BO_Sub:
-    return -SE->getRHS();
-  default:
-    // We cannot simplify non-additive operators.
-    return DefaultAdjustment;
+      // Don't forget to negate the adjustment if it's being subtracted.
+      // This should happen /after/ promotion, in case the value being
+      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
+      if (Op == BO_Sub)
+        Adjustment = -Adjustment;
+    }
   }
 }
 
@@ -246,6 +230,12 @@
   assert(BinaryOperator::isComparisonOp(op) &&
          "Non-comparison ops should be rewritten as comparisons to zero.");
 
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
+
+  // Get the type used for calculating wraparound.
+  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx));
+
   // We only handle simple comparisons of the form "$sym == constant"
   // or "($sym+constant1) == constant2".
   // The adjustment is "constant1" in the above expression. It's used to
@@ -254,28 +244,12 @@
   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
   // the subclasses of SimpleConstraintManager to handle the adjustment.
   SymbolRef Sym = LHS;
-  llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  computeAdjustment(Sym, Adjustment);
 
-  // FIXME: This next section is a hack. It silently converts the integers to
-  // be of the same type as the symbol, which is not always correct. Really the
-  // comparisons should be performed using the Int's type, then mapped back to
-  // the symbol's range of values.
-  ProgramStateManager &StateMgr = state->getStateManager();
-  ASTContext &Ctx = StateMgr.getContext();
-
-  QualType T = Sym->getType(Ctx);
-  assert(T->isIntegerType() || Loc::isLocType(T));
-  unsigned bitwidth = Ctx.getTypeSize(T);
-  bool isSymUnsigned 
-    = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);
-
-  // Convert the adjustment.
-  Adjustment.setIsUnsigned(isSymUnsigned);
-  Adjustment = Adjustment.extOrTrunc(bitwidth);
-
-  // Convert the right-hand side integer.
-  llvm::APSInt ConvertedInt(Int, isSymUnsigned);
-  ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
+  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
 
   switch (op) {
   default:
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index e082d9d..088d70c 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
@@ -23,8 +23,10 @@
 
 class SimpleConstraintManager : public ConstraintManager {
   SubEngine &SU;
+  BasicValueFactory &BVF;
 public:
-  SimpleConstraintManager(SubEngine &subengine) : SU(subengine) {}
+  SimpleConstraintManager(SubEngine &subengine, BasicValueFactory &BV)
+    : SU(subengine), BVF(BV) {}
   virtual ~SimpleConstraintManager();
 
   //===------------------------------------------------------------------===//
@@ -79,6 +81,8 @@
   // Internal implementation.
   //===------------------------------------------------------------------===//
 
+  BasicValueFactory &getBasicVals() const { return BVF; }
+
   bool canReasonAbout(SVal X) const;
 
   ProgramStateRef assumeAux(ProgramStateRef state,
diff --git a/test/Analysis/additive-folding-range-constraints.c b/test/Analysis/additive-folding-range-constraints.c
index 056110f..a64c910 100644
--- a/test/Analysis/additive-folding-range-constraints.c
+++ b/test/Analysis/additive-folding-range-constraints.c
@@ -6,6 +6,9 @@
 void free(void *);
 #define NULL ((void*)0)
 #define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (-INT_MAX - 1)
+
 
 // Each of these adjusted ranges has an adjustment small enough to split the
 // solution range across an overflow boundary (Min for <, Max for >).
@@ -97,3 +100,158 @@
     free(b);
   return; // no-warning
 }
+
+
+// Test the nine cases in RangeConstraintManager's pinning logic.
+void mixedComparisons1(signed char a) {
+  // Case 1: The range is entirely below the symbol's range.
+  int min = INT_MIN;
+
+  if ((a - 2) < (min + 5LL))
+    return; // expected-warning{{never executed}}
+
+  if (a == 0)
+    return; // no-warning
+  if (a == 0x7F)
+    return; // no-warning
+  if (a == -0x80)
+    return; // no-warning
+  return; // no-warning
+}
+
+void mixedComparisons2(signed char a) {
+  // Case 2: Only the lower end of the range is outside.
+  if ((a - 5) < (-0x81LL)) {
+    if (a == 0)
+      return; // expected-warning{{never executed}}
+    if (a == 0x7F)
+      return; // expected-warning{{never executed}}
+    if (a == -0x80)
+      return; // no-warning    
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons3(signed char a) {
+  // Case 3: The entire symbol range is covered.
+  if ((a - 0x200) < -0x100LL) {
+    if (a == 0)
+      return; // no-warning
+    if (a == 0x7F)
+      return; // no-warning
+    if (a == -0x80)
+      return; // no-warning    
+    return; // no-warning
+  } else {
+    return; // expected-warning{{never executed}}
+  }
+}
+
+void mixedComparisons4(signed char a) {
+  // Case 4: The range wraps around, but the lower wrap is out-of-range.
+  if ((a - 5) > 0LL) {
+    if (a == 0)
+      return; // expected-warning{{never executed}}
+    if (a == 0x7F)
+      return; // no-warning
+    if (a == -0x80)
+      return; // expected-warning{{never executed}}
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons5(signed char a) {
+  // Case 5a: The range is inside and does not wrap.
+  if ((a + 5) == 0LL) {
+    if (a == 0)
+      return; // expected-warning{{never executed}}
+    if (a == 0x7F)
+      return; // expected-warning{{never executed}}
+    if (a == -0x80)
+      return; // expected-warning{{never executed}}
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons5Wrap(signed char a) {
+  // Case 5b: The range is inside and does wrap.
+  if ((a + 5) != 0LL) {
+    if (a == 0)
+      return; // no-warning
+    if (a == 0x7F)
+      return; // no-warning
+    if (a == -0x80)
+      return; // no-warning
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons6(signed char a) {
+  // Case 6: Only the upper end of the range is outside.
+  if ((a + 5) > 0x81LL) {
+    if (a == 0)
+      return; // expected-warning{{never executed}}
+    if (a == 0x7F)
+      return; // no-warning
+    if (a == -0x80)
+      return; // expected-warning{{never executed}}
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons7(signed char a) {
+  // Case 7: The range wraps around but is entirely outside the symbol's range.
+  int min = INT_MIN;
+
+  if ((a + 2) < (min + 5LL))
+    return; // expected-warning{{never executed}}
+
+  if (a == 0)
+    return; // no-warning
+  if (a == 0x7F)
+    return; // no-warning
+  if (a == -0x80)
+    return; // no-warning
+  return; // no-warning
+}
+
+void mixedComparisons8(signed char a) {
+  // Case 8: The range wraps, but the upper wrap is out of range.
+  if ((a + 5) < 0LL) {
+    if (a == 0)
+      return; // expected-warning{{never executed}}
+    if (a == 0x7F)
+      return; // expected-warning{{never executed}}
+    if (a == -0x80)
+      return; // no-warning
+    return; // no-warning
+  } else {
+    return; // no-warning
+  }
+}
+
+void mixedComparisons9(signed char a) {
+  // Case 9: The range is entirely above the symbol's range.
+  int max = INT_MAX;
+
+  if ((a + 2) > (max - 5LL))
+    return; // expected-warning{{never executed}}
+
+  if (a == 0)
+    return; // no-warning
+  if (a == 0x7F)
+    return; // no-warning
+  if (a == -0x80)
+    return; // no-warning
+  return; // no-warning
+}
diff --git a/test/Analysis/additive-folding.cpp b/test/Analysis/additive-folding.cpp
index 3c9bf3b..136dc08 100644
--- a/test/Analysis/additive-folding.cpp
+++ b/test/Analysis/additive-folding.cpp
@@ -7,6 +7,8 @@
 void free(void *);
 #define NULL ((void*)0)
 #define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (-INT_MAX - 1)
 
 //---------------
 //  Plus/minus
@@ -203,6 +205,140 @@
 }
 
 
+// Tautologies from outside the range of the symbol
+void tautologyOutsideGT(unsigned char a) {
+  void *b = malloc(1);
+  if (a > 0x100)
+    return; // expected-warning{{never executed}}
+  if (a > -1)
+    free(b);
+  return; // no-warning
+}
+
+void tautologyOutsideGE(unsigned char a) {
+  void *b = malloc(1);
+  if (a >= 0x100)
+    return; // expected-warning{{never executed}}
+  if (a >= -1)
+    free(b);
+  return; // no-warning
+}
+
+void tautologyOutsideLT(unsigned char a) {
+  void *b = malloc(1);
+  if (a < -1)
+    return; // expected-warning{{never executed}}
+  if (a < 0x100)
+    free(b);
+  return; // no-warning
+}
+
+void tautologyOutsideLE (unsigned char a) {
+  void *b = malloc(1);
+  if (a <= -1)
+    return; // expected-warning{{never executed}}
+  if (a <= 0x100)
+    free(b);
+  return; // no-warning
+}
+
+void tautologyOutsideEQ(unsigned char a) {
+  if (a == 0x100)
+    malloc(1); // expected-warning{{never executed}}
+  if (a == -1)
+    malloc(1); // expected-warning{{never executed}}
+}
+
+void tautologyOutsideNE(unsigned char a) {
+  void *sentinel = malloc(1);
+  if (a != 0x100)
+    free(sentinel);
+
+  sentinel = malloc(1);
+  if (a != -1)
+    free(sentinel);
+}
+
+
+// Wraparound with mixed types. Note that the analyzer assumes
+// -fwrapv semantics.
+void mixedWraparoundSanityCheck(int a) {
+  int max = INT_MAX;
+  int min = INT_MIN;
+
+  int b = a + 1;
+  if (a == max && b != min)
+    return; // expected-warning{{never executed}}
+}
+
+void mixedWraparoundGT(int a) {
+  int max = INT_MAX;
+
+  if ((a + 2) > (max + 1LL))
+    return; // expected-warning{{never executed}}
+}
+
+void mixedWraparoundGE(int a) {
+  int max = INT_MAX;
+  int min = INT_MIN;
+
+  if ((a + 2) >= (max + 1LL))
+    return; // expected-warning{{never executed}}
+
+  void *sentinel = malloc(1);
+  if ((a - 2LL) >= min)
+    free(sentinel);
+  return; // expected-warning{{leak}}
+}
+
+void mixedWraparoundLT(int a) {
+  int min = INT_MIN;
+
+  if ((a - 2) < (min - 1LL))
+    return; // expected-warning{{never executed}}
+}
+
+void mixedWraparoundLE(int a) {
+  int max = INT_MAX;
+  int min = INT_MIN;
+
+  if ((a - 2) <= (min - 1LL))
+    return; // expected-warning{{never executed}}
+
+  void *sentinel = malloc(1);
+  if ((a + 2LL) <= max)
+    free(sentinel);
+  return; // expected-warning{{leak}}
+}
+
+void mixedWraparoundEQ(int a) {
+  int max = INT_MAX;
+
+  if ((a + 2) == (max + 1LL))
+    return; // expected-warning{{never executed}}
+}
+
+void mixedWraparoundNE(int a) {
+  int max = INT_MAX;
+
+  void *sentinel = malloc(1);
+  if ((a + 2) != (max + 1LL))
+    free(sentinel);
+  return; // no-warning
+}
+
+
+// Mixed-signedness comparisons.
+void mixedSignedness(int a, unsigned b) {
+  int sMin = INT_MIN;
+  unsigned uMin = INT_MIN;
+  if (a == sMin && a != uMin)
+    return; // expected-warning{{never executed}}
+  if (b == uMin && b != sMin)
+    return; // expected-warning{{never executed}}
+}
+
+
 // PR12206/12510 - When SimpleSValBuilder figures out that a symbol is fully
 // constrained, it should cast the value to the result type in a binary
 // operation...unless the binary operation is a comparison, in which case the
@@ -268,3 +404,13 @@
   if (value == (local + 1))
     malloc(1); // expected-warning{{never executed}}
 }
+
+void multiplicativeSanityTest(int x) {
+  // At one point we were ignoring the *4 completely -- the constraint manager
+  // would see x < 8 and then declare the next part unreachable.
+  if (x*4 < 8)
+    return;
+  if (x == 3)
+    malloc(1);
+  return; // expected-warning{{leak}}
+}
diff --git a/test/Analysis/out-of-bounds.c b/test/Analysis/out-of-bounds.c
index a97bba5..c172170 100644
--- a/test/Analysis/out-of-bounds.c
+++ b/test/Analysis/out-of-bounds.c
@@ -128,11 +128,13 @@
   buf[0][0] = 1; // no-warning
 }
 
-// Testing if solver handles (symbol * constant) < constant
+// *** FIXME ***
+// We don't get a warning here yet because our symbolic constraint solving
+// doesn't handle:  (symbol * constant) < constant
 void test3(int x) {
   int buf[100];
   if (x < 0)
-    buf[x] = 1; // expected-warning {{Out of bound memory access (accessed memory precedes memory block)}}
+    buf[x] = 1;
 }
 
 // *** FIXME ***