[Analyzer] Basic support for multiplication and division in the constraint manager (for == and != only)

[baloghadamsoftware]

Summary

Currently, the default (range-based) constraint manager supports symbolic expressions of the format symbol + integer or symbol - integer to compare them to another integer. However, multiplication and division is not supported yet.

An example where multiplication (and division) could be useful is the checking whether a pointer operation or an array index is out of the bounds of the memory region. The index is often a first-degree expression of the format a*x + b (e.g. for special sparse matrices, such as triangular ones).

In this patch we only support multiplication and division for two kinds of symbolic comparisons: the == and the != operators. The rest is to follow in a subsequent patch. Negative multipliers and divisors are not supported yet.

[baloghadamsoftware]

@NoQ Any comments/concerns regarding this solution?

[baloghadamsoftware]

Tests updated to the now default eagerly assume mode. Range scaling fixed.

[NoQ]

I guess that's roughly the way to go if we want to expand RangeConstraintManager with more math.

One important thing to test here, that doesn't seem to be tested, is what happens when the integer and the scale value are of different types. This may occur because we don't have any representation for integral casts and therefore the type of the symbol itself isn't necessarily the type of the unknown value it represents. As usual, that complicates this sort of work.

I think it's a good idea to organize the constraint manager and SValBuilder a bit better, so that it was easier to understand the algorithmic complexity of the newly implemented stuff by looking at small parts of their code.

Also i'd really appreciate if someone refactors SValBuilder and/or RangeConstraintManager so that it was easier to navigate. The current ad-hoc code structure makes it too hard to figure out what the contract of every function is and how do the changes affect algorithmic complexity of the whole thing. But for this patch it doesn't seem to be that bad.

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

576–597 ↗

(On Diff #174189)

I believe that this code should be moved directly into getRange(). If it's about looking at a single symbol and figuring out what range information about it do we already have, it should go into getRange(). This way we don't need to duplicate it in all the assume...() functions, and also it's exactly what getRange() is supposed to accomplish.

616–617 ↗

(On Diff #174189)

Mmm, what if Scale.Val is veeeeeeeery large?

[baloghadamsoftware]

Thank you for reviewing this patch!

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

576–597 ↗

(On Diff #174189)

getRange() retrieves the existing range for the symbol. However, similarly to the Adjustment we use the Scale to change the right side of the relation, not the left one.

I also dislike code multiplication. Maybe we should use the Strategy pattern here and create a function that does the loop. However, if you take a look at D49074 you will see that the body of the loop may look quite different.

616–617 ↗

(On Diff #174189)

That is a real problem. We either have to limit this functionality for small numbers (for the short term, maybe) or find a better algorithm (for the long term).

[baloghadamsoftware]

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

576–597 ↗

(On Diff #174189)

I took a look again at all the loops including D49074, but only the loop conditions match. There are no other similarities between the loop bodies. I can move the loop into another function taking a lambda as the loop body but it does not simplify the code so I see no point in it.

616–617 ↗

(On Diff #174189)

Any suggestion for the limit? Maybe 256?

[baloghadamsoftware]

Multipliers limited to less or equal to 255.

[baloghadamsoftware]

Intersecting an empty set caused an assertion. Early return inserted to prevent this.

[NoQ]

test/Analysis/multiplicative-folding.c

140–142 ↗

(On Diff #211726)

Something's not right here. All three can potentially be true, because both 1/2 == 0 and (-1)/2 == 0.

[baloghadamsoftware]

Fixed error when the result of an integer division is compared to zero.

[baloghadamsoftware]

test/Analysis/multiplicative-folding.c

140–142 ↗

(On Diff #211726)

Thank you for noticing this! It is strange that I forgot about 0 for == and != but not for the rest of the comparison operators in my subsequent patch. Now I fixed it.

[baloghadamsoftware]

Rebased.

[vabridgers]

ping! Any chance of this patch being accepted? This patch can help some SA false positives.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                           const llvm::APSInt &From,
                                           const llvm::APSInt &To,
                                           bool InRange) override;
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override;
 
 protected:
+  struct ScalingFactor {
+    llvm::APSInt Val;
+    bool Reciprocal;
+  };
+
   /// Assume a constraint between a symbolic expression and a concrete integer.
   virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
                                BinaryOperator::Opcode op,
                                const llvm::APSInt &Int);
 
   //===------------------------------------------------------------------===//
   // Interface that subclasses must implement.
   //===------------------------------------------------------------------===//
 
   // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
   // operation for the method being invoked.
 
   virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
+                                      const ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
+                                      const ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
+  static void computeScale(SymbolRef &Sym, ScalingFactor &Scale);
 };
 
 } // end GR namespace
 
 } // end clang namespace
 
 #endif

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
                  unsigned int Space = 0, bool IsDot = false) const override;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from RangedConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
+                              const ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
+                              const ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(llvm::function_ref<RangeSet()> RS,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
 
+  bool rescale(llvm::APSInt &Int, const ScalingFactor &Scale,
+               const llvm::APSInt &Index);
 };
 
 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
if (SSE->getOpcode() == BO_Sub) {
             T->isSignedIntegerOrEnumerationType())
           return negV;
       }
     }
   }
   return nullptr;
 }
 
+bool RangeConstraintManager::rescale(llvm::APSInt &Int,
+                                     const ScalingFactor &Scale,
+                                     const llvm::APSInt &Index) {
+  if (Scale.Val == 1)
+    return true;
+
+  APSIntType ScaleType(Scale.Val);
+  APSIntType BigType(2 * ScaleType.getBitWidth(), ScaleType.isUnsigned());
+
+  if (Scale.Reciprocal) {
+    // Check whether the scaled value can show up
+    if(ScaleType.testInRange(BigType.convert(Int) * BigType.convert(Scale.Val),
+                             true) != APSIntType::RTR_Within)
+      return false;
+
+    Int = Int * Scale.Val;
+    return true;
+  } else {
+    llvm::APSInt Range = BigType.convert(ScaleType.getMaxValue()) -
+      BigType.convert(ScaleType.getMinValue()) +
+      BigType.getValue(1);
+    llvm::APSInt PeriodInt = Range / BigType.convert(Scale.Val);
+    llvm::APSInt PeriodFrac = Range % BigType.convert(Scale.Val);
+    llvm::APSInt Quotient = BigType.convert(Int) / BigType.convert(Scale.Val);
+    llvm::APSInt Remainder = BigType.convert(Int) % BigType.convert(Scale.Val);
+    llvm::APSInt Frac = Remainder + BigType.convert(Index) * PeriodFrac;
+    Int = ScaleType.convert(Quotient + BigType.convert(Index) * PeriodInt +
+                            Frac / BigType.convert(Scale.Val));
+
+    return (Frac % BigType.convert(Scale.Val)).isNullValue();
+  }
+}
+
 //===------------------------------------------------------------------------===
 // assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
 // and (x, y) for open ranges. These ranges are modular, corresponding with
 // a common treatment of C integer overflow. This means that these methods
 // do not have to worry about overflow; RangeSet::Intersect can handle such a
 // "wraparound" range.
 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
 // UINT_MAX, 0, 1, and 2.
 
 ProgramStateRef
 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     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, true) != APSIntType::RTR_Within)
     return St;
 
-  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
-  llvm::APSInt Upper = Lower;
-  --Lower;
-  ++Upper;
-
-  // [Int-Adjustment+1, Int-Adjustment-1]
+  // [(Int-Adjustment)/Scale+1, (Int-Adjustment)/Scale-1]
   // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
+
+  RangeSet New = getRange(St, Sym);
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+    llvm::APSInt ScInt = AdjInt;
+    if (!rescale(ScInt, Scale, I))
+      continue;
+
+    llvm::APSInt Lower = ScInt;
+    llvm::APSInt Upper = ScInt;
+    Lower--;
+    Upper++;
+
+    if (Scale.Reciprocal) {
+      if (!AdjustmentType.isUnsigned() && ScInt <= 0)
+        Lower -= Scale.Val - AdjustmentType.getValue(1);
+      if (ScInt >= 0)
+        Upper += Scale.Val - AdjustmentType.getValue(1);
+    }
+
+    New = New.Intersect(getBasicVals(), F, Upper, Lower);
+
+    if (New.isEmpty())
+      return nullptr;
+  }
+
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     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, true) != APSIntType::RTR_Within)
     return nullptr;
 
-  // [Int-Adjustment, Int-Adjustment]
+  // [(Int-Adjustment)/Scale, (Int-Adjustment)/Scale]
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
-  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
+
+  RangeSet New = F.getEmptySet();
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+  
+    llvm::APSInt ScInt = AdjInt;
+    if (!rescale(ScInt, Scale, I))
+      continue;
+
+    llvm::APSInt Lower = ScInt;
+    llvm::APSInt Upper = ScInt;
+
+    if (Scale.Reciprocal) {
+      if (!AdjustmentType.isUnsigned() && ScInt <= 0)
+        Lower -= Scale.Val - AdjustmentType.getValue(1);
+      if (ScInt >= 0)
+        Upper += Scale.Val - AdjustmentType.getValue(1);
+    }
+
+    New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+                                                      Upper));
+  }
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymLTRange(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.

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
   QualType T = Sym->getType();
 
   // Non-integer types are not supported.
   if (!T->isIntegralOrEnumerationType())
     return State;
 
   // Reverse the operation and add directly to state.
   const llvm::APSInt &Zero = BVF.getValue(0, T);
+  const ScalingFactor One = {BVF.getValue(1, T), false};
   if (Assumption)
-    return assumeSymNE(State, Sym, Zero, Zero);
+    return assumeSymNE(State, Sym, Zero, One, Zero);
   else
-    return assumeSymEQ(State, Sym, Zero, Zero);
+    return assumeSymEQ(State, Sym, Zero, One, Zero);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
                                                       SymbolRef Sym,
                                                       BinaryOperator::Opcode Op,
                                                       const llvm::APSInt &Int) {
   assert(BinaryOperator::isComparisonOp(Op) &&
          "Non-comparison ops should be rewritten as comparisons to zero.");
 
   // Simplification: translate an assume of a constraint of the form
   // "(exp comparison_op expr) != 0" to true into an assume of
   // "exp comparison_op expr" to true. (And similarly, an assume of the form
   // "(exp comparison_op expr) == 0" to true into an assume of
   // "exp comparison_op expr" to false.)
   if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
     if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
       if (BinaryOperator::isComparisonOp(SE->getOpcode()))
         return assumeSym(State, Sym, (Op == BO_NE ? true : false));
   }
 
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
 
-  // We only handle simple comparisons of the form "$sym == constant"
-  // or "($sym+constant1) == constant2".
+  // We only handle simple comparisons of the form "$sym == constant",
+  // "$sym*constant0 == constant2", "$sym+constant1 == constant2" and
+  // "($sym*constant0)+constant1 == constant2".
+
   // The adjustment is "constant1" in the above expression. It's used to
   // "slide" the solution range around for modular arithmetic. For example,
   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
   // the subclasses of SimpleConstraintManager to handle the adjustment.
   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
   computeAdjustment(Sym, Adjustment);
 
+  // The scale is "constant0" in the above expression. It's used to
+  // "rescale" the solution range. It's up to the subclasses of
+  // SimpleConstraintManager to handle the scaling.
+
+  ScalingFactor Scale = {WraparoundType.getValue(1), false};
+  // FIXME: For now scaling only works for == and !=
+  if (Op == BO_EQ || Op == BO_NE)
+    computeScale(Sym, Scale);
+
   // Convert the right-hand side integer as necessary.
   APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
   llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
 
   // Prefer unsigned comparisons.
   if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) {
+    Scale.Val.setIsSigned(false);
     Adjustment.setIsSigned(false);
+  }
 
   switch (Op) {
   default:
     llvm_unreachable("invalid operation not caught by assertion above");
 
   case BO_EQ:
-    return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymEQ(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_NE:
-    return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymNE(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_GT:
     return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
 
   case BO_GE:
     return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
 
   case BO_LT:
     return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
 
   case BO_LE:
     return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
   } // end switch
 }
 
+void RangedConstraintManager::computeScale(SymbolRef &Sym,
+                                           ScalingFactor &Scale) {
+  // Is it a "($sym*constant1)" expression?
+  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SE->getOpcode();
+    if (Op == BO_Mul || Op == BO_Div) {
+      Sym = SE->getLHS();
+
+      // FIXME: We do not yet support multiplication/division by negative
+      if (SE->getRHS() < 0)
+        return;
+
+      // We cannot handle too big multipliers
+      if (Op == BO_Mul && SE->getRHS() > 255)
+        return;
+
+      Scale.Val = APSIntType(Scale.Val).convert(SE->getRHS());
+
+      // Don't forget to reciprocate the scale if it's being divided.
+      Scale.Reciprocal = (Op == BO_Div);
+    }
+  }
+}
+
 void RangedConstraintManager::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());

clang/test/Analysis/multiplicative-folding.c

+// RUN: %clang_analyze_cc1 --std=c11 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+void clang_analyzer_warnIfReached(void);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (int)(UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (-INT_MAX - 1)
+
+#define ULONG_LONG_MAX (~0UL)
+#define LONG_LONG_MAX (long long)(ULONG_LONG_MAX & (ULONG_LONG_MAX >> 1))
+#define LONG_LONG_MIN (-LONG_LONG_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__))
+
+typedef int int32_t;
+typedef unsigned int uint32_t;
+typedef long long int64_t;
+typedef unsigned long long uint64_t;
+
+void signed_multiplication_eq(int32_t n) {
+  if (n * 2 == 3) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n * 2 == 4) {
+    const int32_t C1 = 0x80000002, C2 = 2;
+    
+    assert(C1 * 2 == 4);
+    assert(C2 * 2 == 4);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n * 3 == 4) {
+    const int32_t C1 = 0xaaaaaaac;
+
+    assert(C1 * 3 == 4);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n * 4 == -5) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n * 4 == -8) {
+    const int32_t C1 = 0xbffffffe, C2 = 0xfffffffe,
+                  C3 = 0x3ffffffe, C4 = 0x7ffffffe;
+
+    assert(C1 * 4 == -8);
+    assert(C2 * 4 == -8);
+    assert(C3 * 4 == -8);
+    assert(C4 * 4 == -8);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C3 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C3); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C3 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C4 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C4); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C4 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n * 6 == -7) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n * 6 == -2) {
+    const int32_t C1 = 0xd5555555, C2 = 0x55555555;
+
+    assert(C1 * 6 == -2);
+    assert(C2 * 6 == -2);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  }
+}
+
+void signed_multiplication_eq64(int64_t n) {
+  if (n * 2 == 4) {
+    const int64_t C1 = 0x8000000000000002, C2 = 2;
+
+    assert(C1 * 2 == 4);
+    assert(C2 * 2 == 4);
+
+    clang_analyzer_eval(n == LONG_LONG_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == LONG_LONG_MAX); //expected-warning{{FALSE}}
+
+  }
+}
+
+void signed_division_eq(int32_t n) {
+  if (n / 2 == 0) {
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n < -1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= -1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= 1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 2 == 3) {
+    const int32_t C = 6;
+
+    assert(C / 2 == 3);
+    assert((C + 1) / 2 == 3);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= C + 1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C + 2); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 3 == -5) {
+    const int32_t C = -15;
+
+    assert(C / 3 == -5);
+    assert((C - 2) / 3 == -5);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C - 3); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= C - 2); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 2 == INT_MAX / 2 + 1) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n / 3 == INT_MIN / 3 - 1) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n / 4 == INT_MAX) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n / 5 == INT_MIN) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  }
+}
+
+void unsigned_multiplication_eq(uint32_t n) {
+  if (n * 2 == 3) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n * 2 == 4) {
+    const uint32_t C1 = 2, C2 = 0x80000002;
+    
+    assert(C1 * 2 == 4);
+    assert(C2 * 2 == 4);
+
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n * 3 == 4) {
+    const uint32_t C1 = 0xaaaaaaac;
+
+    assert(C1 * 3 == 4);
+
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+
+  }
+}
+
+void unsigned_division_eq(uint32_t n) {
+  if (n / 2 == 0) {
+    clang_analyzer_eval(n <= 1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 2 == 3) {
+    const uint32_t C = 6;
+
+    assert(C / 2 == 3);
+    assert((C + 1) / 2 == 3);
+
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= C + 1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C + 2); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 2 == UINT_MAX / 2 + 1) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n / 3 == UINT_MAX) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  }
+}
+
+void signed_multiplication_ne(int32_t n) {
+  if (n * 2 != 3) {
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 1); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 2); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 3); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+
+    if (n * 2 != 4) {
+      const int32_t C1 = 0x80000002, C2 = 2;
+
+      assert(C1 * 2 == 4);
+      assert(C2 * 2 == 4);
+
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+
+      if (n * 3 != 4) {
+        const int32_t C1 = 0xaaaaaaac;
+
+        assert(C1 * 3 == 4);
+
+        clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+        clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                     //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+
+        if (n * 4 != -5) {
+          clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                             //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == -5); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == -2); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == -1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                             //expected-warning@-1{{TRUE}}
+
+          if (n * 4 != -8) {
+            const int32_t C1 = 0xbffffffe, C2 = 0xfffffffe,
+                          C3 = 0x3ffffffe, C4 = 0x7ffffffe;
+
+            assert(C1 * 4 == -8);
+            assert(C2 * 4 == -8);
+            assert(C3 * 4 == -8);
+            assert(C4 * 4 == -8);
+
+            clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                               //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+            clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+            clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C3 - 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C3); //expected-warning{{FALSE}}
+            clang_analyzer_eval(n == C3 + 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C4 - 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == C4); //expected-warning{{FALSE}}
+            clang_analyzer_eval(n == C4 + 1); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                               //expected-warning@-1{{TRUE}}
+
+            if (n * 6 != -7) {
+              clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                                 //expected-warning@-1{{TRUE}}
+              clang_analyzer_eval(n == -1); //expected-warning{{FALSE}}
+                                            //expected-warning@-1{{TRUE}}
+              clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+              clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                                 //expected-warning@-1{{TRUE}}
+
+              if (n * 6 != -2) {
+                const int32_t C1 = 0xd5555555, C2 = 0x55555555;
+
+                assert(C1 * 6 == -2);
+                assert(C2 * 6 == -2);
+
+                clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                                   //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                                  //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                                  //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                             //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+                                                  //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+                                                  //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                                   //expected-warning@-1{{TRUE}}
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void signed_division_ne(int32_t n) {
+  if (n / 2 != 0) {
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == -2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == -1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 2); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+
+    if (n / 2 != 3) {
+      const int32_t C = 6;
+
+      assert(C / 2 == 3);
+      assert((C + 1) / 2 == 3);
+
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C + 1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C + 2); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+
+      if (n / 3 != -5) {
+        const int32_t C = -15;
+
+        assert(C / 3 == -5);
+        assert((C - 2) / 3 == -5);
+
+        clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C - 3); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C - 2); //expected-warning{{FALSE}}
+        clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+        clang_analyzer_eval(n == C); //expected-warning{{FALSE}}
+        clang_analyzer_eval(n == C + 1); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+
+        if (n / 2 != INT_MAX / 2 + 1) {
+          clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                             //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == INT_MAX / 2 + 1); //expected-warning{{FALSE}}
+                                                     //expected-warning@-1{{TRUE}}
+          clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                             //expected-warning@-1{{TRUE}}
+
+          if (n / 3 != INT_MIN / 3 - 1) {
+            clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                               //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == INT_MIN / 3 - 1); //expected-warning{{FALSE}}
+                                                       //expected-warning@-1{{TRUE}}
+            clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                               //expected-warning@-1{{TRUE}}
+
+            if (n / 4 != INT_MAX) {
+              clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                                 //expected-warning@-1{{TRUE}}
+              clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                                 //expected-warning@-1{{TRUE}}
+
+              if (n / 5 != INT_MIN) {
+                clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                                   //expected-warning@-1{{TRUE}}
+                clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                                   //expected-warning@-1{{TRUE}}
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void unsigned_multiplication_ne(uint32_t n) {
+  if (n * 2 != 3) {
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 1); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 2); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == 3); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+
+    if (n * 2 != 4) {
+      const uint32_t C1 = 2, C2 = 0x80000002;
+
+      assert(C1 * 2 == 4);
+      assert(C2 * 2 == 4);
+
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+
+      if (n * 3 != 4) {
+        const uint32_t C1 = 0xaaaaaaac;
+
+        assert(C1 * 3 == 4);
+
+        clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                     //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+        clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                            //expected-warning@-1{{TRUE}}
+
+      }
+    }
+  }
+}
+
+void unsigned_division_ne(uint32_t n) {
+  if (n / 2 != 0) {
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 2); //expected-warning{{FALSE}}
+                                 //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                        //expected-warning@-1{{TRUE}}
+
+    if (n / 2 != 3) {
+      const uint32_t C = 6;
+
+      assert(C / 2 == 3);
+      assert((C + 1) / 2 == 3);
+
+      clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == C); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C + 1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C + 2); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+
+      if (n / 2 != UINT_MAX / 2 + 1) {
+        clang_analyzer_eval(n == UINT_MAX / 2 + 1); //expected-warning{{FALSE}}
+                                                    //expected-warning@-1{{TRUE}}
+        clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                            //expected-warning@-1{{TRUE}}
+
+        if (n / 4 != UINT_MAX) {
+          clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                              //expected-warning@-1{{TRUE}}
+        }
+      }
+    }
+  }
+}
+
+void additive(int32_t n) {
+  if (n * 2 + 1 == 4) {
+    clang_analyzer_warnIfReached(); // no-warning
+
+  } else if (n * 4 - 1 == 15) {
+    const int32_t C1 = 0x80000004, C2 = 0xc0000004, C3 = 4, C4 = 0x40000004;
+
+    assert(C1 * 4 - 1 == 15);
+    assert(C2 * 4 - 1 == 15);
+    assert(C3 * 4 - 1 == 15);
+    assert(C4 * 4 - 1 == 15);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C2); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C2 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C3 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C3); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C3 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C4 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C4); //expected-warning{{FALSE}}
+                                  //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == C4 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 6 + 3 == 7) {
+    const int32_t C = 24;
+
+    assert(C / 6 + 3 == 7);
+    assert((C + 5) / 6 + 3 == 7);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= C + 5); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C + 6); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 5 - 2 == 4) {
+    const int32_t C = 30;
+
+    assert(C / 5 - 2 == 4);
+    assert((C + 4) / 5 - 2 == 4);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n <= C + 4); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C + 5); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n * 3 - INT_MIN == 7) {
+    const int32_t C1 = 0x2aaaaaad;
+
+    assert(C1 * 3 - INT_MIN == 7);
+
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1 - 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == C1); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n == C1 + 1); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+
+  } else if (n / 2 + 1 == INT_MAX / 2 + 1) {
+    clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+    clang_analyzer_eval(n == INT_MAX - 1); //expected-warning{{FALSE}}
+                                           //expected-warning@-1{{TRUE}}
+    clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                       //expected-warning@-1{{TRUE}}
+
+  }
+}
+
+void mixed_signedness(int32_t n, uint32_t m) {
+  if (n * 2U == 4) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (n * 3 == 9U) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (n * 5U == 25U) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 2U == 4) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 3 == 9U) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 5 == 2) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  }
+}
+
+void mixed_size(int32_t n, int64_t m) {
+  if (n * 2L == 4) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (n * 3 == 9L) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (n * 5L == 25L) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 2L == 4) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 3 == 9L) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  } else if (m * 5 == 2) {
+    clang_analyzer_warnIfReached(); //expected-warning{{REACHABLE}}
+  }
+}