[Analyzer] Basic support for multiplication and division in the constraint manager

[baloghadamsoftware]

Summary

Add support for multiplications and divisions of symbols when using comparison operators >, >=, < and <= in the range-based constraint manager.

[baloghadamsoftware]

All existing tests pass. I could not find the appropriate test file so I created a new one, but this is probably not the correct way.

[baloghadamsoftware]

This seems to solve https://bugs.llvm.org/show_bug.cgi?id=32911.

[george.karpenkov]

@baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?

[george.karpenkov]

Let's discuss alternatives first.

[NoQ]

test/Analysis/constraint_manager_scale.c

78 ↗

(On Diff #154578)

If int is 32-bit and x equal to 2³¹ - 1, we have x * 2 equal to -2 which is less than 8, while x is greater than 4.

[george.karpenkov]

The overall point is that writing this kind of code is *extremely* error-prone.
We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues.
Could you see whether Z3 visitor would meet your needs?

[baloghadamsoftware]

In D49074#1156110, @george.karpenkov wrote:

@baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?

As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths. This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

As we discussed with @dcoughlin at the Euro LLVM 2018 the community should consider a new constraint manager, which is in between the range-based one and the Z3 both feature and performance wise. However, this is something long term, until then we should improve the existing one as far as reasonable. I am sure that multiplicative operations can be solved similarly to the additive ones.

test/Analysis/constraint_manager_scale.c

78 ↗

(On Diff #154578)

Thank you for pointing me out this! I uploaded this patch as WIP since I was sure I missed something because of modular arithmetic. I think this can be solved, even if not so easily. Maybe we should restrict the first version to division only?

[baloghadamsoftware]

In D49074#1156609, @george.karpenkov wrote:

The overall point is that writing this kind of code is *extremely* error-prone.

Every modifications on the core is extremely error-prone. That is why we must cross check it and only apply it if it is 100% mathematically correct. This patch is only WIP for now. Freezing the core in its current state helps us to not introduce new errors but also prevents improving the current functionality which is not yet sufficient for many of our customers. What I did is not hacking, multiplicative operations can be implemented a similar way to additive ones, they are just a bit more complex.

We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues.

What issues could it cause since it is guarded by an option? As for the rearrangement of the additive operations it was @NoQ's idea but I agree there. Actually I feel this rearrangement patch a bit of hacking, but I also agree with @NoQ that it may be useful for other checkers as well. That was the reason to put it into SValBuilder instead of the checker itself. As you may be aware of it I originally did the rearrangement inside the checker.

Could you see whether Z3 visitor would meet your needs?

We will look at it, but please read my previous answer.

[baloghadamsoftware]

This comment was removed by baloghadamsoftware.

[george.karpenkov]

What issues could it cause since it is guarded by an option?

I've meant the rearrangement. Actually, I would like to apologize for that point, I thought it was causing some issues, but it wasn't, we've just checked it yesterday.

As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths.

Yes.

This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.

[xazax.hun]

In D49074#1159095, @george.karpenkov wrote:

This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.

This is not an example from the iterator checker (hopefully Adam will provide us with one example from there) but think of division by zero. The division by zero check will only warn if a value is constrained to be zero. The imprecision in the built in solver might result in failure to constrain a value to zero while the Z3 might be able to do that.

[george.karpenkov]

The imprecision in the built in solver might result in failure to constrain a value to zero while the Z3 might be able to do that.

Ah right, that's a good point, we only throw a null-pointer deref/division by zero when the pointer/value is definitely zero.

Do you have *motivating* examples though, like an actual code samples where you got a bug and the analyzer does not warn?
In my experience, we almost never warn about division by zero anyway,
and the null pointer dereference check is too noisy if anything.

[NoQ]

I'd also rather stick to integer arithmetic and avoid using floats even in intermediate calculations. It'd be hard to make sure that no rounding errors kick in if we use floats.

[baloghadamsoftware]

In D49074#1160793, @NoQ wrote:

I'd also rather stick to integer arithmetic and avoid using floats even in intermediate calculations. It'd be hard to make sure that no rounding errors kick in if we use floats.

Yes, I agree. I think an integer plus a flag (whether to take the reciprocal) is better since we only use n or 1/n for scaling.

[baloghadamsoftware]

Completely rewritten: works correctly for modular arithmetic (multiplication), works correctly for truncation (division), only uses integers, no floats.

[george.karpenkov]

@baloghadamsoftware @xazax.hun we've had very promising results with using Z3 for refutation so far, almost at no cost, see Mikhail's recent email on cfe-dev (and sometimes at a negative cost!).
Do you still not want to try it first? False negatives could be addressed as well separately (e.g. by giving a checkers an option to cross-check the report with a more expensive solver before throwing), currently false positives are a far more pressing problem.

[baloghadamsoftware]

Of course we would like to try the Z3 for refutation, we do not dispute its usefulness. This patch is about something really different. It extends the range-based constraint manager in a very natural way. Is the code of the range-based constraint manager frozen for some reason? If not, then why not add multiplication and division as well, where addition and subtraction is already supported?

[george.karpenkov]

where addition and subtraction is already supported?

Is it though? From what I recall we had to disable it from the default set of options due to the fact that it gives rise to the exponential running time in some cases.
I am somewhat afraid of similar unexpected side-effects from this and subsequent patches.

[baloghadamsoftware]

Disabled? No, that was a different thing. I have some ideas there as well, how to solve it, but it was the rearrangement in the SValBuilder. This one is one level lower, the ConstraintManager which only calculate the range for a symbol where we have and assumption for it. Here operations such as Symbol + Integer1 <= Integer2 have been supported for many years (+ can be - as well, similarily we can replace <= with any other comparison operator). This patch adds support for * and / so it extends support for expressions like Symbol * Integer0 + Integer1 <= Integer2. It has marginal impact on the performance, a constant and surely not exponential.

[baloghadamsoftware]

This also solves the examples in the comment of bug 32911.

[baloghadamsoftware]

Since modifications of the infrastructure are always error-prone I tried to generate tests to have full coverage for smaller numbers. However for full coverage I need type signed char and unsigned char, but these tests failed because of this bug: Bug 39138. If that bug is fixed we can have full coverage for both signed and unsigned char types which is more than enough. Of course the generated test should not be part of the standard test suite because of its execution time.

[baloghadamsoftware]

Rebased on the previous part. Tests updated for the now default eagerly assume mode.

[baloghadamsoftware]

Here is the proof of the algorithm for signed char and unsigned char types. The dumper which tests every n for the n*k <comparison operator> m relation and creates ranges from values satisfying the expression for every k and m produces exactly the same output as the generator which generates the ranges using the algorithm from the patch. One the machine I run them they take between 30 and 60 seconds to run.

proof.tar.bz22 KBDownload

[baloghadamsoftware]

Rebased.

[baloghadamsoftware]

I tested this on several open-source projects. Lots of false-positives disappeared. There are also some new findings, mainly new false-positives but not because of this feature but of "loops executed 0 times".

[baloghadamsoftware]

Rebased.

[baloghadamsoftware]

I evaluated this patch on different open-source projects, with Z3 refutation off and on:

MulDivEvaluation.xlsx12 KBDownload

I cannot always decide whether a bug is false positive or true positive. Most of them seem false positives. Honestly, we cannot except too many true positives in these projects. My findings:

• Execution time is largely unaffected. The most interesting thing here is that in one case (PostGreS) Z3 refutation causes 7x execution time with the original range-based constraint manager, but only 1,5x with our patch. The reason for this could be that with the more advanced range-based constraint manager the analyzer does not produce the problematic false positive on which the Z3 refutation spends a huge time.

• In case of Curl and also in case of BitCoin we found false positives not produced with our patch but produced with the original, even with Z3 enabled.

• The extra false positives produced by the analyzer with our patch are not caused by bugs in the implementation of division and multiplication of ranges but the less "unknown" symbolic values. Without the patch the result of a multiplication or division was unknown so the analyzer could not reason about it. Now with the patch it has a valid range so the analyzer can reason about it and report bugs (which may be false positives as well).

[baloghadamsoftware]

Rebased.

[baloghadamsoftware]

We have applied this patch in our internal release and our users have used it for more than half a year without any problems: no crashes, no freezes and no suspicious false positives caused by 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

public:
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override;
 
 protected:
   struct ScalingFactor {
     llvm::APSInt Val;
     bool Reciprocal;
+
+    enum RoundingMode {rmExact, rmDown, rmUp};
   };
 
   /// 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);
 
   //===------------------------------------------------------------------===//
protected:
 
   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 ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
+                                      const ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
+                                      const ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
                                       const llvm::APSInt &V,
+                                      const ScalingFactor &Scale,
                                       const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+      const llvm::APSInt &To, const ScalingFactor &Scale,
+      const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+      const llvm::APSInt &To, const ScalingFactor &Scale,
+      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

public:
 
   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 ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
+                              const ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
+                              const ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
+                              const ScalingFactor &Scale,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+      const llvm::APSInt &To, const ScalingFactor &Scale,
+      const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+      const llvm::APSInt &To, const ScalingFactor &Scale,
+      const llvm::APSInt &Adjustment) override;
 
 private:
   RangeSet::Factory F;
 
   RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
   const RangeSet* getRangeForMinusSymbol(ProgramStateRef State,
                                          SymbolRef Sym);
 
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
+                         const ScalingFactor &Scale,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
+                         const ScalingFactor &Scale,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
+                         const ScalingFactor &Scale,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(llvm::function_ref<RangeSet()> RS,
                          const llvm::APSInt &Int,
+                         const ScalingFactor &Scale,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
+                         const ScalingFactor &Scale,
                          const llvm::APSInt &Adjustment);
 
   bool rescale(llvm::APSInt &Int, const ScalingFactor &Scale,
-               const llvm::APSInt &Index);
+               const llvm::APSInt &Index,
+               const ScalingFactor::RoundingMode Rounding);
 };
 
 } // 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) {
+bool
+RangeConstraintManager::rescale(llvm::APSInt &Int,
+                                const llvm::APSInt &Index,
+                                const ScalingFactor::RoundingMode Rounding) {
   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 (Scale.Reciprocal) {
     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));
 
+    switch(Rounding) {
+    default:
+      llvm_unreachable("Invalid rounding mode!");
+    case ScalingFactor::rmExact:
       return (Frac % BigType.convert(Scale.Val)).isNullValue();
+    case ScalingFactor::rmDown:
+      if (Frac % BigType.convert(Scale.Val) < BigType.getZeroValue()) {
+        --Int;
+      }
+      return true;
+    case ScalingFactor::rmUp:
+      if (Frac % BigType.convert(Scale.Val) > BigType.getZeroValue()) {
+        ++Int;
+      }
+      return true;
+    }
   }
 }
 
 //===------------------------------------------------------------------------===
 // assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
   // Notice that the lower bound is greater than the upper bound.
   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))
+    if (!rescale(ScInt, Scale, I, ScalingFactor::rmExact))
       continue;
 
     llvm::APSInt Lower = ScInt;
     llvm::APSInt Upper = ScInt;
     Lower--;
     Upper++;
 
     if (Scale.Reciprocal) {
RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
   // [(Int-Adjustment)/Scale, (Int-Adjustment)/Scale]
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
 
   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))
+    if (!rescale(ScInt, Scale, I, ScalingFactor::rmExact))
       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 ScalingFactor &Scale,
                                                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, true)) {
   case APSIntType::RTR_Below:
     return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     return getRange(St, Sym);
   }
 
   // Special case for Int == Min. This is always false.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Min = AdjustmentType.getMinValue();
   if (ComparisonVal == Min)
     return F.getEmptySet();
 
-  llvm::APSInt Lower = Min - Adjustment;
-  llvm::APSInt Upper = ComparisonVal - Adjustment;
-  --Upper;
+  llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+  llvm::APSInt AdjMin = Min - Adjustment;
+  RangeSet New = F.getEmptySet();
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+    llvm::APSInt Lower = AdjMin;
+    rescale(Lower, Scale, I, ScalingFactor::rmUp);
+    llvm::APSInt Upper = AdjCompVal;
+    rescale(Upper, Scale, I, ScalingFactor::rmUp);
+    Upper -= (Scale.Reciprocal && Upper <= 0) ? Scale.Val :
+                                               AdjustmentType.getValue(1);
+
+    if (Lower == Upper + AdjustmentType.getValue(1))
+      continue;
+
+    New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+                                                      Upper));
+  }
 
-  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New;
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     const llvm::APSInt &Adjustment) {
-  RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
+  RangeSet New = getSymLTRange(St, Sym, Int, Scale, Adjustment);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(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);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
     return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     return F.getEmptySet();
   }
 
   // Special case for Int == Max. This is always false.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   if (ComparisonVal == Max)
     return F.getEmptySet();
 
-  llvm::APSInt Lower = ComparisonVal - Adjustment;
-  llvm::APSInt Upper = Max - Adjustment;
-  ++Lower;
+  llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+  llvm::APSInt AdjMax = Max - Adjustment;
+  RangeSet New = F.getEmptySet();
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+    llvm::APSInt Lower = AdjCompVal;
+    rescale(Lower, Scale, I, ScalingFactor::rmDown);
+    llvm::APSInt Upper = AdjMax;
+    rescale(Upper, Scale, I, ScalingFactor::rmDown);
+    Lower += (Scale.Reciprocal && Lower >= 0) ? Scale.Val :
+                                               AdjustmentType.getValue(1);
+
+    if (Lower == Upper + AdjustmentType.getValue(1))
+      continue;
+
+    New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+                                                      Upper));
+  }
 
-  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New;
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     const llvm::APSInt &Adjustment) {
-  RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
+  RangeSet New = getSymGTRange(St, Sym, Int, Scale, Adjustment);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymGERange(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);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
     return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     return F.getEmptySet();
   }
 
   // Special case for Int == Min. This is always feasible.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Min = AdjustmentType.getMinValue();
   if (ComparisonVal == Min)
     return getRange(St, Sym);
 
   llvm::APSInt Max = AdjustmentType.getMaxValue();
-  llvm::APSInt Lower = ComparisonVal - Adjustment;
-  llvm::APSInt Upper = Max - Adjustment;
 
-  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+  llvm::APSInt AdjMax = Max - Adjustment;
+  RangeSet New = F.getEmptySet();
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+    llvm::APSInt Lower = AdjCompVal;
+    rescale(Lower, Scale, I, ScalingFactor::rmUp);
+    llvm::APSInt Upper = AdjMax;
+    rescale(Upper, Scale, I, ScalingFactor::rmDown);
+
+    if (Scale.Reciprocal && Lower <= 0) {
+      Lower -= Scale.Val - AdjustmentType.getValue(1);
+    }
+
+    if (Lower == Upper + AdjustmentType.getValue(1))
+      continue;
+
+    New = New.addRange(F, getRange(St, Sym).Intersect(getBasicVals(), F, Lower,
+                                                      Upper));
+  }
+
+  return New;
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     const llvm::APSInt &Adjustment) {
-  RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
+  RangeSet New = getSymGERange(St, Sym, Int, Scale, Adjustment);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymLERange(
       llvm::function_ref<RangeSet()> RS,
       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);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
     return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     return RS();
   }
 
   // Special case for Int == Max. This is always feasible.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   if (ComparisonVal == Max)
     return RS();
 
   llvm::APSInt Min = AdjustmentType.getMinValue();
-  llvm::APSInt Lower = Min - Adjustment;
-  llvm::APSInt Upper = ComparisonVal - Adjustment;
 
-  return RS().Intersect(getBasicVals(), F, Lower, Upper);
+  llvm::APSInt AdjCompVal = ComparisonVal - Adjustment;
+  llvm::APSInt AdjMin = Min - Adjustment;
+  RangeSet New = F.getEmptySet();
+  for (llvm::APSInt I = AdjustmentType.getZeroValue();
+      I < (Scale.Reciprocal ? AdjustmentType.getValue(1) : Scale.Val); ++I) {
+
+    llvm::APSInt Lower = AdjMin;
+    rescale(Lower, Scale, I, ScalingFactor::rmUp);
+    llvm::APSInt Upper = AdjCompVal;
+    rescale(Upper, Scale, I, ScalingFactor::rmDown);
+
+    if (Scale.Reciprocal && Upper >= 0) {
+      Upper += Scale.Val - AdjustmentType.getValue(1);
+    }
+
+    if (Lower == Upper + AdjustmentType.getValue(1))
+      continue;
+
+    New = New.addRange(F, RS().Intersect(getBasicVals(), F, Lower, Upper));
+  }
+
+  return New;
 }
 
 RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
                                                SymbolRef Sym,
                                                const llvm::APSInt &Int,
+                                               const ScalingFactor &Scale,
                                                const llvm::APSInt &Adjustment) {
-  return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment);
+  return getSymLERange([&] { return getRange(St, Sym); }, Int, Scale,
+                       Adjustment);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
+                                    const ScalingFactor &Scale,
                                     const llvm::APSInt &Adjustment) {
-  RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
+  RangeSet New = getSymLERange(St, Sym, Int, Scale, Adjustment);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-    const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
-  RangeSet New = getSymGERange(State, Sym, From, Adjustment);
+    const llvm::APSInt &To, const ScalingFactor &Scale,
+    const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymGERange(State, Sym, From, Scale, Adjustment);
   if (New.isEmpty())
     return nullptr;
-  RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment);
+  RangeSet Out = getSymLERange([&] { return New; }, To, Scale, Adjustment);
   return Out.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, Out);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-    const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
-  RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
-  RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
+    const llvm::APSInt &To, const ScalingFactor &Scale,
+    const llvm::APSInt &Adjustment) {
+  RangeSet RangeLT = getSymLTRange(State, Sym, From, Scale, Adjustment);
+  RangeSet RangeGT = getSymGTRange(State, Sym, To, Scale, Adjustment);
   RangeSet New(RangeLT.addRange(F, RangeGT));
   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
 }
 
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
 

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
 
   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
   SymbolRef AdjustedSym = Sym;
   computeAdjustment(AdjustedSym, Adjustment);
 
+  ScalingFactor Scale = {WraparoundType.getValue(1), false};
+  SymbolRef ScaledSym = AdjustedSym;
+  computeScale(ScaledSym, Scale);
+
   // Convert the right-hand side integer as necessary.
   APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
   llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
   llvm::APSInt ConvertedTo = ComparisonType.convert(To);
 
   // Prefer unsigned comparisons.
   if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) {
+    Scale.Val.setIsSigned(false);
     Adjustment.setIsSigned(false);
+  }
 
   if (InRange)
     return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                         ConvertedTo, Adjustment);
+                                         ConvertedTo, Scale, Adjustment);
   return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                        ConvertedTo, Adjustment);
+                                        ConvertedTo, Scale, Adjustment);
 }
 
 ProgramStateRef
 RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                               SymbolRef Sym, bool Assumption) {
   BasicValueFactory &BVF = getBasicVals();
   QualType T = Sym->getType();
 
ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
   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()) {
     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, Scale, Adjustment);
 
   case BO_NE:
     return assumeSymNE(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_GT:
-    return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymGT(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_GE:
-    return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymGE(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_LT:
-    return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymLT(State, Sym, ConvertedInt, Scale, Adjustment);
 
   case BO_LE:
-    return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
+    return assumeSymLE(State, Sym, ConvertedInt, Scale, 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();

clang/test/Analysis/multiplicative-folding.c

if (n / 2 != 3) {
           clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
                                               //expected-warning@-1{{TRUE}}
         }
       }
     }
   }
 }
 
+void signed_multiplication_lt_0(int32_t n) {
+  if (n * 2 < 3) {
+    int32_t                  U1 = 0x80000001,
+            L2 = 0xc0000000, U2 = 1,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 < 3);
+    assert(U1 * 2 < 3);
+    assert((U1 + 1) * 2 >= 3);
+    assert(L2 * 2 < 3);
+    assert((L2 - 1) * 2 >= 3);
+    assert(U2 * 2 < 3);
+    assert((U2 + 1) * 2 >= 3);
+    assert(L3 * 2 < 3);
+    assert((L3 - 1) * 2 >= 3);
+    assert(INT_MAX * 2 < 3);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2){
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_lt_1(int32_t n) {
+  if (n * 2 < 4) {
+    int32_t                  U1 = 0x80000001,
+            L2 = 0xc0000000, U2 = 1,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 < 4);
+    assert(U1 * 2 < 4);
+    assert((U1 + 1) * 2 >= 4);
+    assert(L2 * 2 < 4);
+    assert((L2 - 1) * 2 >= 4);
+    assert(U2 * 2 < 4);
+    assert((U2 + 1) * 2 >= 4);
+    assert(L3 * 2 < 4);
+    assert((L3 - 1) * 2 >= 4);
+    assert(INT_MAX * 2 < 4);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2){
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_lt_2(int32_t n) {
+  if (n * 2 < 5) {
+    int32_t                  U1 = 0x80000002,
+            L2 = 0xc0000000, U2 = 2,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 < 5);
+    assert(U1 * 2 < 5);
+    assert((U1 + 1) * 2 >= 5);
+    assert(L2 * 2 < 5);
+    assert((L2 - 1) * 2 >= 5);
+    assert(U2 * 2 < 5);
+    assert((U2 + 1) * 2 >= 5);
+    assert(L3 * 2 < 5);
+    assert((L3 - 1) * 2 >= 5);
+    assert(INT_MAX * 2 < 5);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2){
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_lt_3(int32_t n) {
+  if (n * 3 < 4) {
+    int32_t                  U1 = 0xaaaaaaab,
+            L2 = 0xd5555556, U2 = 1,
+            L3 = 0x2aaaaaab, U3 = 0x55555556;
+
+    assert(INT_MIN * 3 < 4);
+    assert(U1 * 3 < 4);
+    assert((U1 + 1) * 3 >= 4);
+    assert(L2 * 3 < 4);
+    assert((L2 - 1) * 3 >= 4);
+    assert(U2 * 3 < 4);
+    assert((U2 + 1) * 3 >= 4);
+    assert(L3 * 3 < 4);
+    assert((L3 - 1) * 3 >= 4);
+    assert(U3 * 3 < 4);
+    assert((U3 + 1) * 3 >= 4);
+
+    if (n < (int32_t) 0xc0000000) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x15555556) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_lt_4(int32_t n) {
+  if (n * 6 < -2) {
+    int32_t L1 = 0x95555556, U1 = 0xaaaaaaaa,
+            L2 = 0xc0000000, U2 = 0x55555554,
+            L3 = 0xeaaaaaab, U3 = -1,
+            L4 = 0x15555556, U4 = 0x2aaaaaaa,
+            L5 = 0x40000000, U5 = 0x55555554,
+            L6 = 0x6aaaaaab;
+
+    assert(L1 * 6 < -2);
+    assert((L1 - 1) * 6 >= -2);
+    assert(U1 * 6 < -2);
+    assert((U1 + 1) * 6 >= -2);
+    assert(L2 * 6 < -2);
+    assert((L2 - 1) * 6 >= -2);
+    assert(U2 * 6 < -2);
+    assert((U2 + 1) * 6 >= -2);
+    assert(L3 * 6 < -2);
+    assert((L3 - 1) * 6 >= -2);
+    assert(U3 * 6 < -2);
+    assert((U3 + 1) * 6 >= -2);
+    assert(L4 * 6 < -2);
+    assert((L4 - 1) * 6 >= -2);
+    assert(U4 * 6 < -2);
+    assert((U4 + 1) * 6 >= -2);
+    assert(L5 * 6 < -2);
+    assert((L5 - 1) * 6 >= -2);
+    assert(U5 * 6 < -2);
+    assert((U5 + 1) * 6 >= -2);
+    assert(L6 * 6 < -2);
+    assert((L6 - 1) * 6 >= -2);
+    assert(INT_MAX * 6 < -2);
+
+    if (n < (int32_t) 0xb5555555) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xdfffffff) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x0aaaaaaa) {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x35555555) {
+      clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x5fffffff) {
+      clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_division_lt_0(int32_t n) {
+  if (n / 4 < 0) {
+    const int32_t C = -4;
+
+    assert(C / 4 < 0);
+    assert((C + 1) / 4 >= 0);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_lt_1(int32_t n) {
+  if (n / 3 < 2) {
+    const int32_t C = 5;
+
+    assert(C / 3 < 2);
+    assert((C + 1) / 3 >= 2);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_lt_2(int32_t n) {
+  if (n / 5 < -7) {
+    const int32_t C = -40;
+
+    assert(C / 5 < -7);
+    assert((C + 1) / 5 >= -7);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_multiplication_lt_0(uint32_t n) {
+  if (n * 2 < 3) {
+    uint32_t                  U1 = 1,
+             L2 = 0x80000000, U2 = 0x80000001;
+
+    assert(U1 * 2 < 3);
+    assert((U1 + 1) * 2 >= 3);
+    assert(L2 * 2 < 3);
+    assert((L2 - 1) * 2 >= 3);
+    assert(U2 * 2 < 3);
+    assert((U2 + 1) * 2 >= 3);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_lt_1(uint32_t n) {
+  if (n * 2 < 4) {
+    uint32_t                  U1 = 1,
+             L2 = 0x80000000, U2 = 0x80000001;
+
+    assert(U1 * 2 < 4);
+    assert((U1 + 1) * 2 >= 4);
+    assert(L2 * 2 < 4);
+    assert((L2 - 1) * 2 >= 4);
+    assert(U2 * 2 < 4);
+    assert((U2 + 1) * 2 >= 4);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_lt_2(uint32_t n) {
+  if (n * 2 < 5) {
+    uint32_t                  U1 = 2,
+             L2 = 0x80000000, U2 = 0x80000002;
+
+    assert(U1 * 2 < 5);
+    assert((U1 + 1) * 2 >= 5);
+    assert(L2 * 2 < 5);
+    assert((L2 - 1) * 2 >= 5);
+    assert(U2 * 2 < 5);
+    assert((U2 + 1) * 2 >= 5);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_lt_3(uint32_t n) {
+  if (n * 3 < 4) {
+    uint32_t U1 = 1, C2 = 0x55555556, C3 = 0xaaaaaaab;
+
+    assert(U1 * 3 < 4);
+    assert((U1 + 1) * 3 >= 4);
+    assert(C2 * 3 < 4);
+    assert((C2 - 1) * 3 >= 4);
+    assert((C2 + 1) * 3 >= 4);
+    assert(C3 * 3 < 4);
+    assert((C3 - 1) * 3 >= 4);
+    assert((C3 + 1) * 3 >= 4);
+
+    if (n < 0x2aaaaaab) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < 0x80000000) {
+      clang_analyzer_eval(n < C2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > C2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < C3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > C3); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_division_lt_0(uint32_t n) {
+  if (n / 3 < 2) {
+    const uint32_t C = 5;
+
+    assert(C / 3 < 2);
+    assert((C + 1) / 3 >= 2);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_multiplication_le_0(int32_t n) {
+  if (n * 2 <= 3) {
+    int32_t                  U1 = 0x80000001,
+            L2 = 0xc0000000, U2 = 1,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 <= 3);
+    assert(U1 * 2 <= 3);
+    assert((U1 + 1) * 2 > 3);
+    assert(L2 * 2 <= 3);
+    assert((L2 - 1) * 2 > 3);
+    assert(U2 * 2 <= 3);
+    assert((U2 + 1) * 2 > 3);
+    assert(L3 * 2 <= 3);
+    assert((L3 - 1) * 2 > 3);
+    assert(INT_MAX * 2 <= 3);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_le_1(int32_t n) {
+  if (n * 2 <= 4) {
+    int32_t                  U1 = 0x80000002,
+            L2 = 0xc0000000, U2 = 2,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 <= 4);
+    assert(U1 * 2 <= 4);
+    assert((U1 + 1) * 2 > 4);
+    assert(L2 * 2 <= 4);
+    assert((L2 - 1) * 2 > 4);
+    assert(U2 * 2 <= 4);
+    assert((U2 + 1) * 2 > 4);
+    assert(L3 * 2 <= 4);
+    assert((L3 - 1) * 2 > 4);
+    assert(INT_MAX * 2 <= 4);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2){
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_le_2(int32_t n) {
+  if (n * 2 <= 5) {
+    int32_t                  U1 = 0x80000002,
+            L2 = 0xc0000000, U2 = 2,
+            L3 = 0x40000000;
+
+    assert(INT_MIN * 2 <= 5);
+    assert(U1 * 2 <= 5);
+    assert((U1 + 1) * 2 > 5);
+    assert(L2 * 2 <= 5);
+    assert((L2 - 1) * 2 > 5);
+    assert(U2 * 2 <= 5);
+    assert((U2 + 1) * 2 > 5);
+    assert(L3 * 2 <= 5);
+    assert((L3 - 1) * 2 > 5);
+    assert(INT_MAX * 2 <= 5);
+
+    if (n < INT_MIN / 2) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_le_3(int32_t n) {
+  if (n * 3 <= 4) {
+    int32_t                  U1 = 0xaaaaaaac,
+            L2 = 0xd5555556, U2 = 1,
+            L3 = 0x2aaaaaab, U3 = 0x55555556;
+
+    assert(INT_MIN * 3 <= 4);
+    assert(U1 * 3 <= 4);
+    assert((U1 + 1) * 3 > 4);
+    assert(L2 * 3 <= 4);
+    assert((L2 - 1) * 3 > 4);
+    assert(U2 * 3 <= 4);
+    assert((U2 + 1) * 3 > 4);
+    assert(L3 * 3 <= 4);
+    assert((L3 - 1) * 3 > 4);
+    assert(U3 * 3 <= 4);
+    assert((U3 + 1) * 3 > 4);
+
+    if (n < (int32_t) 0xc0000001) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x15555556) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_le_4(int32_t n) {
+  if (n * 6 <= -2) {
+    int32_t L1 = 0x95555556, U1 = 0xaaaaaaaa,
+            L2 = 0xc0000000, U2 = 0x55555555,
+            L3 = 0xeaaaaaab, U3 = -1,
+            L4 = 0x15555556, U4 = 0x2aaaaaaa,
+            L5 = 0x40000000, U5 = 0x55555555,
+            L6 = 0x6aaaaaab;
+
+    assert(L1 * 6 <= -2);
+    assert((L1 - 1) * 6 > -2);
+    assert(U1 * 6 <= -2);
+    assert((U1 + 1) * 6 > -2);
+    assert(L2 * 6 <= -2);
+    assert((L2 - 1) * 6 > -2);
+    assert(U2 * 6 <= -2);
+    assert((U2 + 1) * 6 > -2);
+    assert(L3 * 6 <= -2);
+    assert((L3 - 1) * 6 > -2);
+    assert(U3 * 6 <= -2);
+    assert((U3 + 1) * 6 > -2);
+    assert(L4 * 6 <= -2);
+    assert((L4 - 1) * 6 > -2);
+    assert(U4 * 6 <= -2);
+    assert((U4 + 1) * 6 > -2);
+    assert(L5 * 6 <= -2);
+    assert((L5 - 1) * 6 > -2);
+    assert(U5 * 6 <= -2);
+    assert((U5 + 1) * 6 > -2);
+    assert(L6 * 6 <= -2);
+    assert((L6 - 1) * 6 > -2);
+    assert(INT_MAX * 6 <= -2);
+
+    if (n < (int32_t) 0xb5555555) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xe0000000) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x0aaaaaaa) {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x35555555) {
+      clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x60000000) {
+      clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_division_le_0(int32_t n) {
+  if (n / 4 <= 0) {
+    const int32_t C = 3;
+
+    assert(C / 4 <= 0);
+    assert((C + 1) / 4 > 0);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_le_1(int32_t n) {
+  if (n / 3 <= 2) {
+    const int32_t C = 8;
+
+    assert(C / 3 <= 2);
+    assert((C + 1) / 3 > 2);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_le_2(int32_t n) {
+  if (n / 5 <= -7) {
+    const int32_t C = -35;
+
+    assert(C / 5 <= -7);
+    assert((C + 1) / 5 > -7);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_multiplication_le_0(uint32_t n) {
+  if (n * 2 <= 3) {
+    uint32_t                  U1 = 1,
+             L2 = 0x80000000, U2 = 0x80000001;
+
+    assert(U1 * 2 <= 3);
+    assert((U1 + 1) * 2 > 3);
+    assert(L2 * 2 <= 3);
+    assert((L2 - 1) * 2 > 3);
+    assert(U2 * 2 <= 3);
+    assert((U2 + 1) * 2 > 3);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_le_1(uint32_t n) {
+  if (n * 2 <= 4) {
+    uint32_t                  U1 = 2,
+             L2 = 0x80000000, U2 = 0x80000002;
+
+    assert(U1 * 2 <= 4);
+    assert((U1 + 1) * 2 > 4);
+    assert(L2 * 2 <= 4);
+    assert((L2 - 1) * 2 > 4);
+    assert(U2 * 2 <= 4);
+    assert((U2 + 1) * 2 > 4);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_le_2(uint32_t n) {
+  if (n * 2 <= 5) {
+    uint32_t                  U1 = 2,
+             L2 = 0x80000000, U2 = 0x80000002;
+
+    assert(U1 * 2 <= 5);
+    assert((U1 + 1) * 2 > 5);
+    assert(L2 * 2 <= 5);
+    assert((L2 - 1) * 2 > 5);
+    assert(U2 * 2 <= 5);
+    assert((U2 + 1) * 2 > 5);
+
+    if (n < UINT_MAX / 2) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_multiplication_le_3(uint32_t n) {
+  if (n * 3 <= 4) {
+    uint32_t                  U1 = 1,
+                     C2 = 0x55555556,
+             L3 = 0xaaaaaaab, U3 = 0xaaaaaaac;
+
+    assert(U1 * 3 <= 4);
+    assert((U1 + 1) * 3 > 4);
+    assert(C2 * 3 <= 4);
+    assert((C2 - 1) * 3 > 4);
+    assert((C2 + 1) * 3 > 4);
+    assert(L3 * 3 <= 4);
+    assert((L3 - 1) * 3 > 4);
+    assert(U3 * 3 <= 4);
+    assert((U3 + 1) * 3 > 4);
+
+    if (n < 0x2aaaaaab) {
+      clang_analyzer_eval(n == 0); //expected-warning{{FALSE}}
+                                   //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < 0x80000000) {
+      clang_analyzer_eval(n < C2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n == C2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > C2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void unsigned_division_le_0(uint32_t n) {
+  if (n / 4 <= 0) {
+    const uint32_t C = 3;
+
+    assert(C / 4 <= 0);
+    assert((C + 1) / 4 > 0);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_division_le_1(uint32_t n) {
+  if (n / 3 <= 2) {
+    const uint32_t C = 8;
+
+    assert(C / 3 <= 2);
+    assert((C + 1) / 3 > 2);
+
+    clang_analyzer_eval(n <= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n > C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_multiplication_gt_0(int32_t n) {
+  if (n * 2 > 3) {
+    int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+            L2 = 2,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 > 3);
+    assert((L1 - 1) * 2 <= 3);
+    assert(U1 * 2 > 3);
+    assert((U1 + 1) * 2 <= 3);
+    assert(L2 * 2 > 3);
+    assert((L2 - 1) * 2 <= 3);
+    assert(U2 * 2 > 3);
+    assert((U2 + 1) * 2 <= 3);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_gt_1(int32_t n) {
+  if (n * 2 > 4) {
+    int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+            L2 = 3,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 > 4);
+    assert((L1 - 1) * 2 <= 4);
+    assert(U1 * 2 > 4);
+    assert((U1 + 1) * 2 <= 4);
+    assert(L2 * 2 > 4);
+    assert((L2 - 1) * 2 <= 4);
+    assert(U2 * 2 > 4);
+    assert((U2 + 1) * 2 <= 4);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_gt_2(int32_t n) {
+  if (n * 2 > 5) {
+    int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+            L2 = 3,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 > 5);
+    assert((L1 - 1) * 2 <= 5);
+    assert(U1 * 2 > 5);
+    assert((U1 + 1) * 2 <= 5);
+    assert(L2 * 2 > 5);
+    assert((L2 - 1) * 2 <= 5);
+    assert(U2 * 2 > 5);
+    assert((U2 + 1) * 2 <= 5);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_gt_3(int32_t n) {
+  if (n * 3 > 4) {
+    int32_t L1 = 0xaaaaaaad, U1 = 0xd5555555,
+            L2 = 2,          U2 = 0x2aaaaaaa,
+            L3 = 0x55555557;
+
+    assert(L1 * 3 > 4);
+    assert((L1 - 1) * 3 <= 4);
+    assert(U1 * 3 > 4);
+    assert((U1 + 1) * 3 <= 4);
+    assert(L2 * 3 > 4);
+    assert((L2 - 1) * 3 <= 4);
+    assert(U2 * 3 > 4);
+    assert((U2 + 1) * 3 <= 4);
+    assert(L3 * 3 > 4);
+    assert((L3 - 1) * 3 <= 4);
+    assert(INT_MAX * 3 > 4);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_gt_4(int32_t n) {
+  if (n * 6 > -2) {
+    int32_t                  U1 = 0x95555555,
+            L2 = 0xaaaaaaab, U2 = 0xbfffffff,
+            L3 = 0xd5555556, U3 = 0xeaaaaaaa,
+            L4 = 0,          U4 = 0x15555555,
+            L5 = 0x2aaaaaab, U5 = 0x3fffffff,
+            L6 = 0x55555556, U6 = 0x6aaaaaaa;
+
+    assert(INT_MIN * 6 > -2);
+    assert(U1 * 6 > -2);
+    assert((U1 + 1) * 6 <= -2);
+    assert(L2 * 6 > -2);
+    assert((L2 - 1) * 6 <= -2);
+    assert(U2 * 6 > -2);
+    assert((U2 + 1) * 6 <= -2);
+    assert(L3 * 6 > -2);
+    assert((L3 - 1) * 6 <= -2);
+    assert(U3 * 6 > -2);
+    assert((U3 + 1) * 6 <= -2);
+    assert(L4 * 6 > -2);
+    assert((L4 - 1) * 6 <= -2);
+    assert(U4 * 6 > -2);
+    assert((U4 + 1) * 6 <= -2);
+    assert(L5 * 6 > -2);
+    assert((L5 - 1) * 6 <= -2);
+    assert(U5 * 6 > -2);
+    assert((U5 + 1) * 6 <= -2);
+    assert(L6 * 6 > -2);
+    assert((L6 - 1) * 6 <= -2);
+    assert(U6 * 6 > -2);
+    assert((U6 + 1) * 6 <= -2);
+
+    if (n < (int32_t) 0xa0000000) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xcaaaaaaa) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xf5555555) {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x20000000) {
+      clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x4aaaaaaa) {
+      clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U6); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_division_gt_0(int32_t n) {
+  if (n / 4 > 0) {
+    const int32_t C = 4;
+
+    assert(C / 4 > 0);
+    assert((C - 1) / 4 <= 0);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_gt_1(int32_t n) {
+  if (n / 3 > 2) {
+    const int32_t C = 9;
+
+    assert(C / 3 > 2);
+    assert((C - 1) / 3 <= 2);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_gt_2(int32_t n) {
+  if (n / 5 > -7) {
+    const int32_t C = -34;
+
+    assert(C / 5 > -7);
+    assert((C - 1) / 5 <= -7);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_multiplication_gt_0(uint32_t n) {
+  if (n * 2 > 3) {
+    uint32_t L1 = 2,          U1 = 0x7fffffff,
+             L2 = 0x80000002;
+
+    assert(L1 * 2 > 3);
+    assert((L1 - 1) * 2 <= 3);
+    assert(U1 * 2 > 3);
+    assert((U1 + 1) * 2 <= 3);
+    assert(L2 * 2 > 3);
+    assert((L2 - 1) * 2 <= 3);
+    assert(UINT_MAX * 2 > 3);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_gt_1(uint32_t n) {
+  if (n * 2 > 4) {
+    uint32_t L1 = 3,          U1 = 0x7fffffff,
+             L2 = 0x80000003;
+
+    assert(L1 * 2 > 4);
+    assert((L1 - 1) * 2 <= 4);
+    assert(U1 * 2 > 4);
+    assert((U1 + 1) * 2 <= 4);
+    assert(L2 * 2 > 4);
+    assert((L2 - 1) * 2 <= 4);
+    assert(UINT_MAX * 2 > 4);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_gt_2(uint32_t n) {
+  if (n * 2 > 5) {
+    uint32_t L1 = 3,          U1 = 0x7fffffff,
+             L2 = 0x80000003;
+
+    assert(L1 * 2 > 5);
+    assert((L1 - 1) * 2 <= 5);
+    assert(U1 * 2 > 5);
+    assert((U1 + 1) * 2 <= 5);
+    assert(L2 * 2 > 5);
+    assert((L2 - 1) * 2 <= 5);
+    assert(UINT_MAX * 2 > 5);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_gt_3(uint32_t n) {
+  if (n * 3 > 4) {
+    uint32_t L1 = 2,          U1 = 0x55555555,
+             L2 = 0x55555557, U2 = 0xaaaaaaaa,
+             L3 = 0xaaaaaaad;
+
+    assert(L1 * 3 > 4);
+    assert((L1 - 1) * 3 <= 4);
+    assert(U1 * 3 > 4);
+    assert((U1 + 1) * 3 <= 4);
+    assert(L2 * 3 > 4);
+    assert((L2 - 1) * 3 <= 4);
+    assert(U2 * 3 > 4);
+    assert((U2 + 1) * 3 <= 4);
+    assert(L3 * 3 > 4);
+    assert((L3 - 1) * 3 <= 4);
+    assert(INT_MAX * 3 > 4);
+
+    if (n < UINT_MAX / 3 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < 2 * (UINT_MAX / 3 + 1)) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_division_gt_0(uint32_t n) {
+  if (n / 4 > 0) {
+    const uint32_t C = 4;
+
+    assert(C / 4 > 0);
+    assert((C - 1) / 4 <= 0);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_division_gt_1(uint32_t n) {
+  if (n / 3 > 2) {
+    const uint32_t C = 9;
+
+    assert(C / 3 > 2);
+    assert((C - 1) / 3 <= 2);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_multiplication_ge_0(int32_t n) {
+  if (n * 2 >= 3) {
+    int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+            L2 = 2,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 >= 3);
+    assert((L1 - 1) * 2 < 3);
+    assert(U1 * 2 >= 3);
+    assert((U1 + 1) * 2 < 3);
+    assert(L2 * 2 >= 3);
+    assert((L2 - 1) * 2 < 3);
+    assert(U2 * 2 >= 3);
+    assert((U2 + 1) * 2 < 3);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_ge_1(int32_t n) {
+  if (n * 2 >= 4) {
+    int32_t L1 = 0x80000002, U1 = 0xbfffffff,
+            L2 = 2,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 >= 4);
+    assert((L1 - 1) * 2 < 4);
+    assert(U1 * 2 >= 4);
+    assert((U1 + 1) * 2 < 4);
+    assert(L2 * 2 >= 4);
+    assert((L2 - 1) * 2 < 4);
+    assert(U2 * 2 >= 4);
+    assert((U2 + 1) * 2 < 4);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_ge_2(int32_t n) {
+  if (n * 2 >= 5) {
+    int32_t L1 = 0x80000003, U1 = 0xbfffffff,
+            L2 = 3,          U2 = 0x3fffffff;
+
+    assert(L1 * 2 >= 5);
+    assert((L1 - 1) * 2 < 5);
+    assert(U1 * 2 >= 5);
+    assert((U1 + 1) * 2 < 5);
+    assert(L2 * 2 >= 5);
+    assert((L2 - 1) * 2 < 5);
+    assert(U2 * 2 >= 5);
+    assert((U2 + 1) * 2 < 5);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_multiplication_ge_3(int32_t n) {
+  if (n * 3 >= 4) {
+    int32_t L1 = 0xaaaaaaac, U1 = 0xd5555555,
+            L2 = 2,          U2 = 0x2aaaaaaa,
+            L3 = 0x55555557;
+
+    assert(L1 * 3 >= 4);
+    assert((L1 - 1) * 3 < 4);
+    assert(U1 * 3 >= 4);
+    assert((U1 + 1) * 3 < 4);
+    assert(L2 * 3 >= 4);
+    assert((L2 - 1) * 3 < 4);
+    assert(U2 * 3 >= 4);
+    assert((U2 + 1) * 3 < 4);
+    assert(L3 * 3 >= 4);
+    assert((L3 - 1) * 3 < 4);
+    assert(INT_MAX * 3 >= 4);
+
+    if (n < 0) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < INT_MAX / 2) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == INT_MAX); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void signed_multiplication_ge_4(int32_t n) {
+  if (n * 6 >= -2) {
+    int32_t                  U1 = 0x95555555,
+            L2 = 0xaaaaaaab, U2 = 0xbfffffff,
+            L3 = 0xd5555555, U3 = 0xeaaaaaaa,
+            L4 = 0,          U4 = 0x15555555,
+            L5 = 0x2aaaaaab, U5 = 0x3fffffff,
+            L6 = 0x55555555, U6 = 0x6aaaaaaa;
+
+    assert(INT_MIN * 6 >= -2);
+    assert(U1 * 6 >= -2);
+    assert((U1 + 1) * 6 < -2);
+    assert(L2 * 6 >= -2);
+    assert((L2 - 1) * 6 < -2);
+    assert(U2 * 6 >= -2);
+    assert((U2 + 1) * 6 < -2);
+    assert(L3 * 6 >= -2);
+    assert((L3 - 1) * 6 < -2);
+    assert(U3 * 6 >= -2);
+    assert((U3 + 1) * 6 < -2);
+    assert(L4 * 6 >= -2);
+    assert((L4 - 1) * 6 < -2);
+    assert(U4 * 6 >= -2);
+    assert((U4 + 1) * 6 < -2);
+    assert(L5 * 6 >= -2);
+    assert((L5 - 1) * 6 < -2);
+    assert(U5 * 6 >= -2);
+    assert((U5 + 1) * 6 < -2);
+    assert(L6 * 6 >= -2);
+    assert((L6 - 1) * 6 < -2);
+    assert(U6 * 6 >= -2);
+    assert((U6 + 1) * 6 < -2);
+
+    if (n < (int32_t) 0xa0000000) {
+      clang_analyzer_eval(n == INT_MIN); //expected-warning{{FALSE}}
+                                         //expected-warning@-1{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xcaaaaaaa) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0xf5555555) {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U3); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x20000000) {
+      clang_analyzer_eval(n < L4); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U4); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U4); //expected-warning{{FALSE}}
+    } else if (n < (int32_t) 0x4aaaaaaa) {
+      clang_analyzer_eval(n < L5); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U5); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U5); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L6); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U6); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U6); //expected-warning{{FALSE}}
+    }
+  }
+}
+
+void signed_division_ge_0(int32_t n) {
+  if (n / 4 >= 0) {
+    const int32_t C = -3;
+
+    assert(C / 4 >= 0);
+    assert((C - 1) / 4 < 0);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_ge_1(int32_t n) {
+  if (n / 3 >= 2) {
+    const int32_t C = 6;
+
+    assert(C / 3 >= 2);
+    assert((C - 1) / 3 < 2);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void signed_division_ge_2(int32_t n) {
+  if (n / 5 >= -7) {
+    const int32_t C = -39;
+
+    assert(C / 5 >= -7);
+    assert((C - 1) / 5 < -7);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
+void unsigned_multiplication_ge_0(uint32_t n) {
+  if (n * 2 >= 3) {
+    uint32_t L1 = 2,          U1 = 0x7fffffff,
+             L2 = 0x80000002;
+
+    assert(L1 * 2 >= 3);
+    assert((L1 - 1) * 2 < 3);
+    assert(U1 * 2 >= 3);
+    assert((U1 + 1) * 2 < 3);
+    assert(L2 * 2 >= 3);
+    assert((L2 - 1) * 2 < 3);
+    assert(UINT_MAX * 2 >= 3);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_ge_1(uint32_t n) {
+  if (n * 2 >= 4) {
+    uint32_t L1 = 2,          U1 = 0x7fffffff,
+             L2 = 0x80000002;
+
+    assert(L1 * 2 >= 4);
+    assert((L1 - 1) * 2 < 4);
+    assert(U1 * 2 >= 4);
+    assert((U1 + 1) * 2 < 4);
+    assert(L2 * 2 >= 4);
+    assert((L2 - 1) * 2 < 4);
+    assert(UINT_MAX * 2 >= 4);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_ge_2(uint32_t n) {
+  if (n * 2 >= 5) {
+    uint32_t L1 = 3,          U1 = 0x7fffffff,
+             L2 = 0x80000003;
+
+    assert(L1 * 2 >= 5);
+    assert((L1 - 1) * 2 < 5);
+    assert(U1 * 2 >= 5);
+    assert((U1 + 1) * 2 < 5);
+    assert(L2 * 2 >= 5);
+    assert((L2 - 1) * 2 < 5);
+    assert(UINT_MAX * 2 >= 5);
+
+    if (n < UINT_MAX / 2 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_multiplication_ge_3(uint32_t n) {
+  if (n * 3 >= 4) {
+    uint32_t L1 = 2,          U1 = 0x55555555,
+             L2 = 0x55555557, U2 = 0xaaaaaaaa,
+             L3 = 0xaaaaaaac;
+
+    assert(L1 * 3 >= 4);
+    assert((L1 - 1) * 3 < 4);
+    assert(U1 * 3 >= 4);
+    assert((U1 + 1) * 3 < 4);
+    assert(L2 * 3 >= 4);
+    assert((L2 - 1) * 3 < 4);
+    assert(U2 * 3 >= 4);
+    assert((U2 + 1) * 3 < 4);
+    assert(L3 * 3 >= 4);
+    assert((L3 - 1) * 3 < 4);
+    assert(INT_MAX * 3 >= 4);
+
+    if (n < UINT_MAX / 3 + 1) {
+      clang_analyzer_eval(n < L1); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U1); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U1); //expected-warning{{FALSE}}
+    } else if (n < 2 * (UINT_MAX / 3 + 1)) {
+      clang_analyzer_eval(n < L2); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n <= U2); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n > U2); //expected-warning{{FALSE}}
+    } else {
+      clang_analyzer_eval(n < L3); //expected-warning{{FALSE}}
+      clang_analyzer_eval(n >= L3); //expected-warning{{TRUE}}
+      clang_analyzer_eval(n == UINT_MAX); //expected-warning{{FALSE}}
+                                          //expected-warning@-1{{TRUE}}
+    }
+  }
+}
+
+void unsigned_division_ge_0(uint32_t n) {
+  if (n / 3 >= 2) {
+    const uint32_t C = 6;
+
+    assert(C / 3 >= 2);
+    assert((C - 1) / 3 < 2);
+
+    clang_analyzer_eval(n >= C); //expected-warning{{TRUE}}
+    clang_analyzer_eval(n < C); //expected-warning{{FALSE}}
+  }
+}
+
 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);