From 71bf61ac00c500b451eb8edd92cb080b8bb20574 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Thu, 27 Jun 2024 12:44:07 +0200
Subject: [PATCH 1/6] SimpleRangeAnalysis lib/: float -> BigInt

---
 .../SimpleRangeAnalysisDefinition.qll         |   4 +-
 .../interfaces/SimpleRangeAnalysisExpr.qll    |   8 +-
 .../ConstantBitwiseAndExprRange.qll           |  17 +-
 .../extensions/ConstantShiftExprRange.qll     |  66 ++-
 .../extensions/StrlenLiteralRangeExpr.qll     |   8 +-
 .../rangeanalysis/extensions/SubtractSelf.qll |   4 +-
 cpp/ql/lib/semmle/code/cpp/commons/Printf.qll |  52 +-
 .../cpp/rangeanalysis/PointlessComparison.qll |  46 +-
 .../cpp/rangeanalysis/RangeAnalysisUtils.qll  | 133 +++--
 .../cpp/rangeanalysis/SimpleRangeAnalysis.qll | 457 +++++++++---------
 .../rangeanalysis/new/SimpleRangeAnalysis.qll |   4 +-
 11 files changed, 432 insertions(+), 367 deletions(-)

diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisDefinition.qll b/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisDefinition.qll
index 12361228202d..d68207f2d370 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisDefinition.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisDefinition.qll
@@ -50,7 +50,7 @@ abstract class SimpleRangeAnalysisDefinition extends RangeSsaDefinition {
    * `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
    * recursive calls to get the bounds of their dependencies.
    */
-  abstract float getLowerBounds(StackVariable v);
+  abstract QlBuiltins::BigInt getLowerBounds(StackVariable v);
 
   /**
    * Gets the upper bound of the variable `v` defined by this definition.
@@ -59,7 +59,7 @@ abstract class SimpleRangeAnalysisDefinition extends RangeSsaDefinition {
    * `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
    * recursive calls to get the bounds of their dependencies.
    */
-  abstract float getUpperBounds(StackVariable v);
+  abstract QlBuiltins::BigInt getUpperBounds(StackVariable v);
 }
 
 import SimpleRangeAnalysisInternal
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisExpr.qll b/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisExpr.qll
index c8c1110b3af8..018286417efb 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisExpr.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/models/interfaces/SimpleRangeAnalysisExpr.qll
@@ -21,7 +21,7 @@ abstract class SimpleRangeAnalysisExpr extends Expr {
    * `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
    * recursive calls to get the bounds of their children.
    */
-  abstract float getLowerBounds();
+  abstract QlBuiltins::BigInt getLowerBounds();
 
   /**
    * Gets the upper bound of the expression.
@@ -30,7 +30,7 @@ abstract class SimpleRangeAnalysisExpr extends Expr {
    * `getFullyConvertedLowerBounds` and `getFullyConvertedUpperBounds` for
    * recursive calls to get the bounds of their children.
    */
-  abstract float getUpperBounds();
+  abstract QlBuiltins::BigInt getUpperBounds();
 
   /**
    * Holds if the range this expression depends on the definition `srcDef` for
@@ -70,9 +70,9 @@ private class Empty extends SimpleRangeAnalysisExpr {
     this = this and none()
   }
 
-  override float getLowerBounds() { none() }
+  override QlBuiltins::BigInt getLowerBounds() { none() }
 
-  override float getUpperBounds() { none() }
+  override QlBuiltins::BigInt getUpperBounds() { none() }
 
   override predicate dependsOnChild(Expr child) { none() }
 }
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantBitwiseAndExprRange.qll b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantBitwiseAndExprRange.qll
index 20e3f6abb17f..2372062f4c2c 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantBitwiseAndExprRange.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantBitwiseAndExprRange.qll
@@ -46,34 +46,37 @@ private class ConstantBitwiseAndExprRange extends SimpleRangeAnalysisExpr {
     result = this.(AssignAndExpr).getRValue()
   }
 
-  override float getLowerBounds() {
+  override QlBuiltins::BigInt getLowerBounds() {
     // If an operand can have negative values, the lower bound is unconstrained.
     // Otherwise, the lower bound is zero.
-    exists(float lLower, float rLower |
+    exists(QlBuiltins::BigInt lLower, QlBuiltins::BigInt rLower |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
       (
-        (lLower < 0 or rLower < 0) and
+        (lLower < 0.toBigInt() or rLower < 0.toBigInt()) and
         result = exprMinVal(this)
         or
         // This technically results in two lowerBounds when an operand range is negative, but
         // that's fine since `exprMinVal(x) <= 0`. We can't use an if statement here without
         // non-monotonic recursion issues
-        result = 0
+        result = 0.toBigInt()
       )
     )
   }
 
-  override float getUpperBounds() {
+  override QlBuiltins::BigInt getUpperBounds() {
     // If an operand can have negative values, the upper bound is unconstrained.
     // Otherwise, the upper bound is the minimum of the upper bounds of the operands
-    exists(float lLower, float lUpper, float rLower, float rUpper |
+    exists(
+      QlBuiltins::BigInt lLower, QlBuiltins::BigInt lUpper, QlBuiltins::BigInt rLower,
+      QlBuiltins::BigInt rUpper
+    |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       lUpper = getFullyConvertedUpperBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
       rUpper = getFullyConvertedUpperBounds(this.getRightOperand()) and
       (
-        (lLower < 0 or rLower < 0) and
+        (lLower < 0.toBigInt() or rLower < 0.toBigInt()) and
         result = exprMaxVal(this)
         or
         // This technically results in two upperBounds when an operand range is negative, but
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantShiftExprRange.qll b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantShiftExprRange.qll
index 3f300d7aa8d6..7939f9edf89d 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantShiftExprRange.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/ConstantShiftExprRange.qll
@@ -2,14 +2,14 @@ private import cpp
 private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr
 private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
-float evaluateConstantExpr(Expr e) {
-  result = e.getValue().toFloat()
+QlBuiltins::BigInt evaluateConstantExpr(Expr e) {
+  result = parseAsBigInt(e.getValue())
   or
   // This handles when a constant value is put into a variable
   // and the variable is used later
   exists(SsaDefinition defn, StackVariable sv |
     defn.getAUse(sv) = e and
-    result = defn.getDefiningValue(sv).getValue().toFloat()
+    result = parseAsBigInt(defn.getDefiningValue(sv).getValue())
   )
 }
 
@@ -18,16 +18,18 @@ float evaluateConstantExpr(Expr e) {
 // architecture where the shift value is masked with 0b00011111, but we can't
 // assume the architecture).
 bindingset[val]
-private predicate isValidShiftExprShift(float val, Expr l) {
-  val >= 0 and
+private predicate isValidShiftExprShift(QlBuiltins::BigInt val, Expr l) {
+  val >= 0.toBigInt() and
   // We use getFullyConverted because the spec says to use the *promoted* left operand
-  val < (l.getFullyConverted().getUnderlyingType().getSize() * 8)
+  val < (l.getFullyConverted().getUnderlyingType().getSize() * 8).toBigInt()
 }
 
 bindingset[val, shift, max_val]
-private predicate canLShiftOverflow(int val, int shift, int max_val) {
+private predicate canLShiftOverflow(
+  QlBuiltins::BigInt val, QlBuiltins::BigInt shift, QlBuiltins::BigInt max_val
+) {
   // val << shift = val * 2^shift > max_val => val > max_val/2^shift = max_val >> b
-  val > max_val.bitShiftRight(shift)
+  val > max_val.bitShiftRightSigned(shift.toInt())
 }
 
 /**
@@ -65,7 +67,7 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
         exists(evaluateConstantExpr(l)) and not exists(evaluateConstantExpr(r))
         or
         // If the right operand is a constant, check if it is a valid shift expression
-        exists(float constROp |
+        exists(QlBuiltins::BigInt constROp |
           constROp = evaluateConstantExpr(r) and isValidShiftExprShift(constROp, l)
         )
       )
@@ -82,8 +84,11 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
     result = this.(AssignRShiftExpr).getRValue()
   }
 
-  override float getLowerBounds() {
-    exists(int lLower, int lUpper, int rLower, int rUpper |
+  override QlBuiltins::BigInt getLowerBounds() {
+    exists(
+      QlBuiltins::BigInt lLower, QlBuiltins::BigInt lUpper, QlBuiltins::BigInt rLower,
+      QlBuiltins::BigInt rUpper
+    |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       lUpper = getFullyConvertedUpperBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
@@ -92,7 +97,7 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
       rLower <= rUpper
     |
       if
-        lLower < 0
+        lLower < 0.toBigInt()
         or
         not (
           isValidShiftExprShift(rLower, this.getLeftOperand()) and
@@ -105,12 +110,15 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
         result = exprMinVal(this)
       else
         // We can get the smallest value by shifting the smallest bound by the largest bound
-        result = lLower.bitShiftRight(rUpper)
+        result = lLower.bitShiftRightSigned(rUpper.toInt())
     )
   }
 
-  override float getUpperBounds() {
-    exists(int lLower, int lUpper, int rLower, int rUpper |
+  override QlBuiltins::BigInt getUpperBounds() {
+    exists(
+      QlBuiltins::BigInt lLower, QlBuiltins::BigInt lUpper, QlBuiltins::BigInt rLower,
+      QlBuiltins::BigInt rUpper
+    |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       lUpper = getFullyConvertedUpperBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
@@ -119,7 +127,7 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
       rLower <= rUpper
     |
       if
-        lLower < 0
+        lLower < 0.toBigInt()
         or
         not (
           isValidShiftExprShift(rLower, this.getLeftOperand()) and
@@ -132,7 +140,7 @@ class ConstantRShiftExprRange extends SimpleRangeAnalysisExpr {
         result = exprMaxVal(this)
       else
         // We can get the largest value by shifting the largest bound by the smallest bound
-        result = lUpper.bitShiftRight(rLower)
+        result = lUpper.bitShiftRightSigned(rLower.toInt())
     )
   }
 
@@ -178,7 +186,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
         exists(evaluateConstantExpr(l)) and not exists(evaluateConstantExpr(r))
         or
         // If the right operand is a constant, check if it is a valid shift expression
-        exists(float constROp |
+        exists(QlBuiltins::BigInt constROp |
           constROp = evaluateConstantExpr(r) and isValidShiftExprShift(constROp, l)
         )
       )
@@ -195,8 +203,11 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
     result = this.(AssignLShiftExpr).getRValue()
   }
 
-  override float getLowerBounds() {
-    exists(int lLower, int lUpper, int rLower, int rUpper |
+  override QlBuiltins::BigInt getLowerBounds() {
+    exists(
+      QlBuiltins::BigInt lLower, QlBuiltins::BigInt lUpper, QlBuiltins::BigInt rLower,
+      QlBuiltins::BigInt rUpper
+    |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       lUpper = getFullyConvertedUpperBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
@@ -205,7 +216,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
       rLower <= rUpper
     |
       if
-        lLower < 0
+        lLower < 0.toBigInt()
         or
         not (
           isValidShiftExprShift(rLower, this.getLeftOperand()) and
@@ -222,12 +233,15 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
         // If necessary, we may be able to improve this bound in the future
         if canLShiftOverflow(lUpper, rUpper, exprMaxVal(this))
         then result = exprMinVal(this)
-        else result = lLower.bitShiftLeft(rLower)
+        else result = lLower.bitShiftLeft(rLower.toInt())
     )
   }
 
-  override float getUpperBounds() {
-    exists(int lLower, int lUpper, int rLower, int rUpper |
+  override QlBuiltins::BigInt getUpperBounds() {
+    exists(
+      QlBuiltins::BigInt lLower, QlBuiltins::BigInt lUpper, QlBuiltins::BigInt rLower,
+      QlBuiltins::BigInt rUpper
+    |
       lLower = getFullyConvertedLowerBounds(this.getLeftOperand()) and
       lUpper = getFullyConvertedUpperBounds(this.getLeftOperand()) and
       rLower = getFullyConvertedLowerBounds(this.getRightOperand()) and
@@ -236,7 +250,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
       rLower <= rUpper
     |
       if
-        lLower < 0
+        lLower < 0.toBigInt()
         or
         not (
           isValidShiftExprShift(rLower, this.getLeftOperand()) and
@@ -253,7 +267,7 @@ class ConstantLShiftExprRange extends SimpleRangeAnalysisExpr {
         // If necessary, we may be able to improve this bound in the future
         if canLShiftOverflow(lUpper, rUpper, exprMaxVal(this))
         then result = exprMaxVal(this)
-        else result = lUpper.bitShiftLeft(rUpper)
+        else result = lUpper.bitShiftLeft(rUpper.toInt())
     )
   }
 
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/StrlenLiteralRangeExpr.qll b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/StrlenLiteralRangeExpr.qll
index f301263d0e38..2c2ad03f42ef 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/StrlenLiteralRangeExpr.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/StrlenLiteralRangeExpr.qll
@@ -10,9 +10,13 @@ class StrlenLiteralRangeExpr extends SimpleRangeAnalysisExpr, FunctionCall {
     this.getTarget().hasGlobalOrStdName("strlen") and this.getArgument(0).isConstant()
   }
 
-  override int getLowerBounds() { result = this.getArgument(0).getValue().length() }
+  override QlBuiltins::BigInt getLowerBounds() {
+    result = this.getArgument(0).getValue().length().toBigInt()
+  }
 
-  override int getUpperBounds() { result = this.getArgument(0).getValue().length() }
+  override QlBuiltins::BigInt getUpperBounds() {
+    result = this.getArgument(0).getValue().length().toBigInt()
+  }
 
   override predicate dependsOnChild(Expr e) { none() }
 }
diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/SubtractSelf.qll b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/SubtractSelf.qll
index 32b4d2a4fba6..5c8051b529e1 100644
--- a/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/SubtractSelf.qll
+++ b/cpp/ql/lib/experimental/semmle/code/cpp/rangeanalysis/extensions/SubtractSelf.qll
@@ -7,9 +7,9 @@ private class SelfSub extends SimpleRangeAnalysisExpr, SubExpr {
       this.getRightOperand().getExplicitlyConverted().(VariableAccess).getTarget()
   }
 
-  override float getLowerBounds() { result = 0 }
+  override QlBuiltins::BigInt getLowerBounds() { result = 0.toBigInt() }
 
-  override float getUpperBounds() { result = 0 }
+  override QlBuiltins::BigInt getUpperBounds() { result = 0.toBigInt() }
 
   override predicate dependsOnChild(Expr child) { none() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll b/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll
index 51d2e294b36e..c6be50c19831 100644
--- a/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll
+++ b/cpp/ql/lib/semmle/code/cpp/commons/Printf.qll
@@ -356,10 +356,8 @@ class FormattingFunctionCall extends Expr {
  * `f` is assumed to be nonnegative.
  */
 bindingset[f]
-private int lengthInBase10(float f) {
-  f = 0 and result = 1
-  or
-  result = f.log10().floor() + 1
+private QlBuiltins::BigInt lengthInBase10(QlBuiltins::BigInt f) {
+  result = f.toString().length().toBigInt()
 }
 
 pragma[nomagic]
@@ -373,7 +371,7 @@ private BufferWriteEstimationReason getEstimationReasonForIntegralExpression(Exp
   // expr should already be given as getFullyConverted
   if
     upperBound(expr) < exprMaxVal(expr) and
-    (exprMinVal(expr) >= 0 or lowerBound(expr) > exprMinVal(expr))
+    (exprMinVal(expr) >= 0.toBigInt() or lowerBound(expr) > exprMinVal(expr))
   then
     // next we check whether the estimate may have been widened
     if upperBoundMayBeWidened(expr)
@@ -1174,31 +1172,32 @@ class FormatLiteral extends Literal instanceof StringLiteral {
         or
         this.getConversionChar(n).toLowerCase() = ["d", "i"] and
         // e.g. -2^31 = "-2147483648"
-        exists(float typeBasedBound, float valueBasedBound |
+        exists(QlBuiltins::BigInt typeBasedBound, QlBuiltins::BigInt valueBasedBound |
           // The first case handles length sub-specifiers
           // Subtract one in the exponent because one bit is for the sign.
           // Add 1 to account for the possible sign in the output.
           typeBasedBound =
-            1 + lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8 - 1)) and
+            1.toBigInt() +
+              lengthInBase10(2.toBigInt().pow(this.getIntegralDisplayType(n).getSize() * 8 - 1)) and
           // The second case uses range analysis to deduce a length that's shorter than the length
           // of the number -2^31.
-          exists(Expr arg, float lower, float upper |
+          exists(Expr arg, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper |
             arg = this.getUse().getConversionArgument(n) and
             lower = lowerBound(arg.getFullyConverted()) and
             upper = upperBound(arg.getFullyConverted())
           |
             valueBasedBound =
-              max(int cand |
+              max(QlBuiltins::BigInt cand |
                 // Include the sign bit in the length if it can be negative
                 (
-                  if lower < 0
-                  then cand = 1 + lengthInBase10(lower.abs())
+                  if lower < 0.toBigInt()
+                  then cand = 1.toBigInt() + lengthInBase10(lower.abs())
                   else cand = lengthInBase10(lower)
                 )
                 or
                 (
-                  if upper < 0
-                  then cand = 1 + lengthInBase10(upper.abs())
+                  if upper < 0.toBigInt()
+                  then cand = 1.toBigInt() + lengthInBase10(upper.abs())
                   else cand = lengthInBase10(upper)
                 )
               ) and
@@ -1206,26 +1205,28 @@ class FormatLiteral extends Literal instanceof StringLiteral {
             // to detect non-trivial range analysis without taking into account up-casting
             reason = getEstimationReasonForIntegralExpression(arg)
           ) and
-          len = valueBasedBound.minimum(typeBasedBound)
+          len = valueBasedBound.minimum(typeBasedBound).toInt()
         )
         or
         this.getConversionChar(n).toLowerCase() = "u" and
         // e.g. 2^32 - 1 = "4294967295"
-        exists(float typeBasedBound, float valueBasedBound |
+        exists(QlBuiltins::BigInt typeBasedBound, QlBuiltins::BigInt valueBasedBound |
           // The first case handles length sub-specifiers
-          typeBasedBound = lengthInBase10(2.pow(this.getIntegralDisplayType(n).getSize() * 8) - 1) and
+          typeBasedBound =
+            lengthInBase10(2.toBigInt().pow(this.getIntegralDisplayType(n).getSize() * 8) -
+                1.toBigInt()) and
           // The second case uses range analysis to deduce a length that's shorter than
           // the length of the number 2^31 - 1.
-          exists(Expr arg, float lower, float upper |
+          exists(Expr arg, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper |
             arg = this.getUse().getConversionArgument(n) and
             lower = lowerBound(arg.getFullyConverted()) and
             upper = upperBound(arg.getFullyConverted())
           |
             valueBasedBound =
-              lengthInBase10(max(float cand |
+              lengthInBase10(max(QlBuiltins::BigInt cand |
                   // If lower can be negative we use `(unsigned)-1` as the candidate value.
-                  lower < 0 and
-                  cand = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
+                  lower < 0.toBigInt() and
+                  cand = 2.toBigInt().pow(any(IntType t | t.isUnsigned()).getSize() * 8)
                   or
                   cand = upper
                 )) and
@@ -1233,7 +1234,7 @@ class FormatLiteral extends Literal instanceof StringLiteral {
             // to detect non-trivial range analysis without taking into account up-casting
             reason = getEstimationReasonForIntegralExpression(arg)
           ) and
-          len = valueBasedBound.minimum(typeBasedBound)
+          len = valueBasedBound.minimum(typeBasedBound).toInt()
         )
         or
         this.getConversionChar(n).toLowerCase() = "x" and
@@ -1250,7 +1251,10 @@ class FormatLiteral extends Literal instanceof StringLiteral {
                 digits = 2 * t.getSize()
               )
             ) and
-          exists(Expr arg, float lower, float upper, float typeLower, float typeUpper |
+          exists(
+            Expr arg, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper,
+            QlBuiltins::BigInt typeLower, QlBuiltins::BigInt typeUpper
+          |
             arg = this.getUse().getConversionArgument(n) and
             lower = lowerBound(arg.getFullyConverted()) and
             upper = upperBound(arg.getFullyConverted()) and
@@ -1260,10 +1264,10 @@ class FormatLiteral extends Literal instanceof StringLiteral {
             valueBasedBound =
               lengthInBase16(max(float cand |
                   // If lower can be negative we use `(unsigned)-1` as the candidate value.
-                  lower < 0 and
+                  lower < 0.toBigInt() and
                   cand = 2.pow(any(IntType t | t.isUnsigned()).getSize() * 8)
                   or
-                  cand = upper
+                  cand = upper.toString().toFloat()
                 )) and
             (
               if lower > typeLower or upper < typeUpper
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/PointlessComparison.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/PointlessComparison.qll
index 47289c7552b9..b90b842666b5 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/PointlessComparison.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/PointlessComparison.qll
@@ -6,10 +6,10 @@ import cpp
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 
 /** Gets the lower bound of the fully converted expression. */
-private float lowerBoundFC(Expr expr) { result = lowerBound(expr.getFullyConverted()) }
+private QlBuiltins::BigInt lowerBoundFC(Expr expr) { result = lowerBound(expr.getFullyConverted()) }
 
 /** Gets the upper bound of the fully converted expression. */
-private float upperBoundFC(Expr expr) { result = upperBound(expr.getFullyConverted()) }
+private QlBuiltins::BigInt upperBoundFC(Expr expr) { result = upperBound(expr.getFullyConverted()) }
 
 /**
  * Describes which side of a pointless comparison is known to be smaller.
@@ -33,7 +33,9 @@ newtype SmallSide =
  * Note that the comparison operation could be any binary comparison
  * operator, for example,`==`, `>`, or `<=`.
  */
-private predicate alwaysLT(ComparisonOperation cmp, float left, float right, SmallSide ss) {
+private predicate alwaysLT(
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, SmallSide ss
+) {
   ss = LeftIsSmaller() and
   left = upperBoundFC(cmp.getLeftOperand()) and
   right = lowerBoundFC(cmp.getRightOperand()) and
@@ -49,19 +51,13 @@ private predicate alwaysLT(ComparisonOperation cmp, float left, float right, Sma
  * Note that the comparison operation could be any binary comparison
  * operator, for example,`==`, `>`, or `<=`.
  */
-private predicate alwaysLE(ComparisonOperation cmp, float left, float right, SmallSide ss) {
+private predicate alwaysLE(
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, SmallSide ss
+) {
   ss = LeftIsSmaller() and
   left = upperBoundFC(cmp.getLeftOperand()) and
   right = lowerBoundFC(cmp.getRightOperand()) and
-  left <= right and
-  // Range analysis is not able to precisely represent large 64 bit numbers,
-  // because it stores the range as a `float`, which only has a 53 bit mantissa.
-  // For example, the number `2^64-1` is rounded to `2^64`. This means that we
-  // cannot trust the result if the numbers are large. Note: there is only
-  // a risk of a rounding error causing an incorrect result if `left == right`.
-  // If `left` is strictly less than `right` then there is enough of a gap
-  // that we don't need to worry about rounding errors.
-  left.ulp() <= 1
+  left <= right
 }
 
 /**
@@ -73,7 +69,9 @@ private predicate alwaysLE(ComparisonOperation cmp, float left, float right, Sma
  * Note that the comparison operation could be any binary comparison
  * operator, for example,`==`, `>`, or `<=`.
  */
-private predicate alwaysGT(ComparisonOperation cmp, float left, float right, SmallSide ss) {
+private predicate alwaysGT(
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, SmallSide ss
+) {
   ss = RightIsSmaller() and
   left = lowerBoundFC(cmp.getLeftOperand()) and
   right = upperBoundFC(cmp.getRightOperand()) and
@@ -89,19 +87,13 @@ private predicate alwaysGT(ComparisonOperation cmp, float left, float right, Sma
  * Note that the comparison operation could be any binary comparison
  * operator, for example,`==`, `>`, or `<=`.
  */
-private predicate alwaysGE(ComparisonOperation cmp, float left, float right, SmallSide ss) {
+private predicate alwaysGE(
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, SmallSide ss
+) {
   ss = RightIsSmaller() and
   left = lowerBoundFC(cmp.getLeftOperand()) and
   right = upperBoundFC(cmp.getRightOperand()) and
-  left >= right and
-  // Range analysis is not able to precisely represent large 64 bit numbers,
-  // because it stores the range as a `float`, which only has a 53 bit mantissa.
-  // For example, the number 2^64-1 is rounded to 2^64. This means that we
-  // cannot trust the result if the numbers are large. Note: there is only
-  // a risk of a rounding error causing an incorrect result if `left == right`.
-  // If `left` is strictly less than `right` then there is enough of a gap
-  // that we don't need to worry about rounding errors.
-  left.ulp() <= 1
+  left >= right
 }
 
 /**
@@ -123,7 +115,8 @@ private predicate alwaysGE(ComparisonOperation cmp, float left, float right, Sma
  * `pointlessComparison(x < y, 9, 7, false, RightIsSmaller)` holds.
  */
 predicate pointlessComparison(
-  ComparisonOperation cmp, float left, float right, boolean value, SmallSide ss
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, boolean value,
+  SmallSide ss
 ) {
   alwaysLT(cmp.(LTExpr), left, right, ss) and value = true
   or
@@ -164,7 +157,8 @@ predicate pointlessComparison(
  *   }
  */
 predicate reachablePointlessComparison(
-  ComparisonOperation cmp, float left, float right, boolean value, SmallSide ss
+  ComparisonOperation cmp, QlBuiltins::BigInt left, QlBuiltins::BigInt right, boolean value,
+  SmallSide ss
 ) {
   pointlessComparison(cmp, left, right, value, ss) and
   // Reachable according to control flow analysis.
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
index eb167a09c4c4..0b11a25bc3d9 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
@@ -235,9 +235,9 @@ predicate eqZeroWithNegate(Expr cmp, Expr a, boolean isEQ, boolean branch) {
  * number. This takes into account the associativity, commutativity and
  * distributivity of arithmetic operations.
  */
-predicate linearAccess(Expr expr, VariableAccess v, float p, float q) {
+predicate linearAccess(Expr expr, VariableAccess v, QlBuiltins::BigInt p, QlBuiltins::BigInt q) {
   // Exclude 0 and NaN.
-  (p < 0 or p > 0) and
+  (p < 0.toBigInt() or p > 0.toBigInt()) and
   linearAccessImpl(expr, v, p, q)
 }
 
@@ -246,34 +246,36 @@ predicate linearAccess(Expr expr, VariableAccess v, float p, float q) {
  * This takes into account the associativity, commutativity and
  * distributivity of arithmetic operations.
  */
-private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q) {
+private predicate linearAccessImpl(
+  Expr expr, VariableAccess v, QlBuiltins::BigInt p, QlBuiltins::BigInt q
+) {
   // Base case
-  expr = v and p = 1.0 and q = 0.0
+  expr = v and p = 1.toBigInt() and q = 0.toBigInt()
   or
-  expr.(ReferenceDereferenceExpr).getExpr() = v and p = 1.0 and q = 0.0
+  expr.(ReferenceDereferenceExpr).getExpr() = v and p = 1.toBigInt() and q = 0.toBigInt()
   or
   // a+(p*v+b) == p*v + (a+b)
-  exists(AddExpr addExpr, float a, float b |
+  exists(AddExpr addExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b |
     addExpr.getLeftOperand().isConstant() and
-    a = addExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
+    a = parseAsBigInt(addExpr.getLeftOperand().getFullyConverted().getValue()) and
     linearAccess(addExpr.getRightOperand(), v, p, b) and
     expr = addExpr and
     q = a + b
   )
   or
   // (p*v+a)+b == p*v + (a+b)
-  exists(AddExpr addExpr, float a, float b |
+  exists(AddExpr addExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b |
     addExpr.getRightOperand().isConstant() and
-    b = addExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
+    b = parseAsBigInt(addExpr.getRightOperand().getFullyConverted().getValue()) and
     linearAccess(addExpr.getLeftOperand(), v, p, a) and
     expr = addExpr and
     q = a + b
   )
   or
   // a-(m*v+b) == -m*v + (a-b)
-  exists(SubExpr subExpr, float a, float b, float m |
+  exists(SubExpr subExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b, QlBuiltins::BigInt m |
     subExpr.getLeftOperand().isConstant() and
-    a = subExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
+    a = parseAsBigInt(subExpr.getLeftOperand().getFullyConverted().getValue()) and
     linearAccess(subExpr.getRightOperand(), v, m, b) and
     expr = subExpr and
     p = -m and
@@ -281,9 +283,9 @@ private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q
   )
   or
   // (p*v+a)-b == p*v + (a-b)
-  exists(SubExpr subExpr, float a, float b |
+  exists(SubExpr subExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b |
     subExpr.getRightOperand().isConstant() and
-    b = subExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
+    b = parseAsBigInt(subExpr.getRightOperand().getFullyConverted().getValue()) and
     linearAccess(subExpr.getLeftOperand(), v, p, a) and
     expr = subExpr and
     q = a - b
@@ -314,7 +316,7 @@ private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q
   )
   or
   // -(a*v+b) == -a*v + (-b)
-  exists(UnaryMinusExpr unaryMinusExpr, float a, float b |
+  exists(UnaryMinusExpr unaryMinusExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b |
     linearAccess(unaryMinusExpr.getOperand().getFullyConverted(), v, a, b) and
     expr = unaryMinusExpr and
     p = -a and
@@ -322,9 +324,9 @@ private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q
   )
   or
   // m*(a*v+b) == (m*a)*v + (m*b)
-  exists(MulExpr mulExpr, float a, float b, float m |
+  exists(MulExpr mulExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b, QlBuiltins::BigInt m |
     mulExpr.getLeftOperand().isConstant() and
-    m = mulExpr.getLeftOperand().getFullyConverted().getValue().toFloat() and
+    m = parseAsBigInt(mulExpr.getLeftOperand().getFullyConverted().getValue()) and
     linearAccess(mulExpr.getRightOperand(), v, a, b) and
     expr = mulExpr and
     p = m * a and
@@ -332,9 +334,9 @@ private predicate linearAccessImpl(Expr expr, VariableAccess v, float p, float q
   )
   or
   // (a*v+b)*m == (m*a)*v + (m*b)
-  exists(MulExpr mulExpr, float a, float b, float m |
+  exists(MulExpr mulExpr, QlBuiltins::BigInt a, QlBuiltins::BigInt b, QlBuiltins::BigInt m |
     mulExpr.getRightOperand().isConstant() and
-    m = mulExpr.getRightOperand().getFullyConverted().getValue().toFloat() and
+    m = parseAsBigInt(mulExpr.getRightOperand().getFullyConverted().getValue()) and
     linearAccess(mulExpr.getLeftOperand(), v, a, b) and
     expr = mulExpr and
     p = m * a and
@@ -368,13 +370,13 @@ predicate cmpWithLinearBound(
   RelationDirection direction, // Is this a lower or an upper bound?
   boolean branch // Which control-flow branch is this bound valid on?
 ) {
-  exists(Expr lhs, float p, RelationDirection dir |
+  exists(Expr lhs, QlBuiltins::BigInt p, RelationDirection dir |
     linearAccess(lhs, v, p, _) and
     relOpWithSwapAndNegate(guard, lhs, _, dir, _, branch) and
     (
-      p > 0 and direction = dir
+      p > 0.toBigInt() and direction = dir
       or
-      p < 0 and direction = negateDirection(dir)
+      p < 0.toBigInt() and direction = negateDirection(dir)
     )
   )
   or
@@ -391,23 +393,23 @@ predicate cmpWithLinearBound(
  * For example, if `t` is a signed 32-bit type then holds if `lb` is
  * `-2^31` and `ub` is `2^31 - 1`.
  */
-private predicate typeBounds(ArithmeticType t, float lb, float ub) {
-  exists(IntegralType integralType, float limit |
-    integralType = t and limit = 2.pow(8 * integralType.getSize())
+private predicate typeBounds(ArithmeticType t, QlBuiltins::BigInt lb, QlBuiltins::BigInt ub) {
+  exists(IntegralType integralType, QlBuiltins::BigInt limit |
+    integralType = t and limit = 2.toBigInt().pow(8 * integralType.getSize())
   |
     if integralType instanceof BoolType
-    then lb = 0 and ub = 1
+    then lb = 0.toBigInt() and ub = 1.toBigInt()
     else
       if integralType.isSigned()
       then (
-        lb = -(limit / 2) and ub = (limit / 2) - 1
+        lb = -(limit / 2.toBigInt()) and ub = (limit / 2.toBigInt()) - 1.toBigInt()
       ) else (
-        lb = 0 and ub = limit - 1
+        lb = 0.toBigInt() and ub = limit - 1.toBigInt()
       )
   )
   or
   // This covers all floating point types. The range is (-Inf, +Inf).
-  t instanceof FloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
+  t instanceof FloatingPointType and lb = -infinityAsBigInt() and ub = infinityAsBigInt()
 }
 
 private Type stripReference(Type t) {
@@ -423,7 +425,7 @@ Type getVariableRangeType(StackVariable v) { result = stripReference(v.getUnspec
  * For example, if `t` is a signed 32-bit type then the result is
  * `-2^31`.
  */
-float typeLowerBound(Type t) { typeBounds(stripReference(t), result, _) }
+QlBuiltins::BigInt typeLowerBound(Type t) { typeBounds(stripReference(t), result, _) }
 
 /**
  * Gets the upper bound for the unspecified type `t`.
@@ -431,7 +433,7 @@ float typeLowerBound(Type t) { typeBounds(stripReference(t), result, _) }
  * For example, if `t` is a signed 32-bit type then the result is
  * `2^31 - 1`.
  */
-float typeUpperBound(Type t) { typeBounds(stripReference(t), _, result) }
+QlBuiltins::BigInt typeUpperBound(Type t) { typeBounds(stripReference(t), _, result) }
 
 /**
  * Gets the minimum value that this expression could represent, based on
@@ -444,7 +446,7 @@ float typeUpperBound(Type t) { typeBounds(stripReference(t), _, result) }
  * `exprMinVal(expr)` you will normally want to call
  * `exprMinVal(expr.getFullyConverted())`.
  */
-float exprMinVal(Expr expr) { result = typeLowerBound(expr.getUnspecifiedType()) }
+QlBuiltins::BigInt exprMinVal(Expr expr) { result = typeLowerBound(expr.getUnspecifiedType()) }
 
 /**
  * Gets the maximum value that this expression could represent, based on
@@ -457,7 +459,7 @@ float exprMinVal(Expr expr) { result = typeLowerBound(expr.getUnspecifiedType())
  * `exprMaxVal(expr)` you will normally want to call
  * `exprMaxVal(expr.getFullyConverted())`.
  */
-float exprMaxVal(Expr expr) { result = typeUpperBound(expr.getUnspecifiedType()) }
+QlBuiltins::BigInt exprMaxVal(Expr expr) { result = typeUpperBound(expr.getUnspecifiedType()) }
 
 /**
  * Gets the minimum value that this variable could represent, based on
@@ -466,7 +468,7 @@ float exprMaxVal(Expr expr) { result = typeUpperBound(expr.getUnspecifiedType())
  * For example, if `v` has a signed 32-bit type then the result is
  * `-2^31`.
  */
-float varMinVal(Variable v) { result = typeLowerBound(v.getUnspecifiedType()) }
+QlBuiltins::BigInt varMinVal(Variable v) { result = typeLowerBound(v.getUnspecifiedType()) }
 
 /**
  * Gets the maximum value that this variable could represent, based on
@@ -475,4 +477,67 @@ float varMinVal(Variable v) { result = typeLowerBound(v.getUnspecifiedType()) }
  * For example, if `v` has a signed 32-bit type then the result is
  * `2^31 - 1`.
  */
-float varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecifiedType()) }
+QlBuiltins::BigInt varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecifiedType()) }
+
+/**
+ * Magic number larger than the largest positive finite double.
+ */
+QlBuiltins::BigInt infinityAsBigInt() { result = 1.toBigInt().bitShiftLeft(1024) }
+
+bindingset[s]
+QlBuiltins::BigInt parseAsBigInt(string s) {
+  result = s.toBigInt()
+  or
+  s.toFloat() = 1.0 / 0.0 and result = infinityAsBigInt()
+  or
+  s.toFloat() = -(1.0 / 0.0) and result = -infinityAsBigInt()
+  or
+  exists(QlBuiltins::BigInt coeff, int base10exp | parseFiniteAsBigInt(s, coeff, base10exp) |
+    if base10exp < 0
+    then result = coeff / 10.toBigInt().pow(-base10exp)
+    else result = coeff * 10.toBigInt().pow(base10exp)
+  )
+}
+
+bindingset[s]
+private predicate parseFiniteAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
+  exists(string t | s = "+" + t | parseUnsignedAsBigInt(t, coeff, base10exp))
+  or
+  exists(string t | s = "-" + t | parseUnsignedAsBigInt(t, -coeff, base10exp))
+  or
+  parseUnsignedAsBigInt(s, coeff, base10exp)
+}
+
+bindingset[s]
+private predicate parseUnsignedAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
+  exists(string beforeE, int base10expAfterE, int base10expBeforeE |
+    beforeE = s.toUpperCase().splitAt("E", 0) and
+    base10expAfterE = parseSignedInt(s.toUpperCase().splitAt("E", 1)) and
+    parseUnsignedDecimalAsBigInt(beforeE, coeff, base10expBeforeE) and
+    base10exp = base10expBeforeE + base10expAfterE
+  )
+  or
+  exists(string beforeDot, string afterDot |
+    beforeDot = s.splitAt(".", 0) and
+    afterDot = s.splitAt(".", 1) and
+    coeff = (beforeDot + afterDot).toBigInt() and
+    base10exp = -afterDot.length()
+  )
+}
+
+bindingset[s]
+private predicate parseUnsignedDecimalAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
+  exists(string beforeDot, string afterDot |
+    beforeDot = s.splitAt(".", 0) and
+    afterDot = s.splitAt(".", 1) and
+    coeff = (beforeDot + afterDot).toBigInt() and
+    base10exp = -afterDot.length()
+  )
+}
+
+bindingset[s]
+private int parseSignedInt(string s) {
+  exists(string t | s = "+" + t | result = t.toInt())
+  or
+  result = s.toInt()
+}
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
index 990def8b2f1c..510a81e87b44 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
@@ -60,37 +60,37 @@ private import NanAnalysis
  * bounds to the set if it helps on specific examples and does not make
  * performance dramatically worse on large codebases, such as libreoffice.
  */
-private float wideningLowerBounds(ArithmeticType t) {
-  result = 2.0 or
-  result = 1.0 or
-  result = 0.0 or
-  result = -1.0 or
-  result = -2.0 or
-  result = -8.0 or
-  result = -16.0 or
-  result = -128.0 or
-  result = -256.0 or
-  result = -32768.0 or
-  result = -65536.0 or
+private QlBuiltins::BigInt wideningLowerBounds(ArithmeticType t) {
+  result = 2.toBigInt() or
+  result = 1.toBigInt() or
+  result = 0.toBigInt() or
+  result = -1.toBigInt() or
+  result = -2.toBigInt() or
+  result = -8.toBigInt() or
+  result = -16.toBigInt() or
+  result = -128.toBigInt() or
+  result = -256.toBigInt() or
+  result = -32768.toBigInt() or
+  result = -65536.toBigInt() or
   result = typeLowerBound(t) or
-  result = -(1.0 / 0.0) // -Inf
+  result = -infinityAsBigInt() // -Inf
 }
 
 /** See comment for `wideningLowerBounds`, above. */
-private float wideningUpperBounds(ArithmeticType t) {
-  result = -2.0 or
-  result = -1.0 or
-  result = 0.0 or
-  result = 1.0 or
-  result = 2.0 or
-  result = 7.0 or
-  result = 15.0 or
-  result = 127.0 or
-  result = 255.0 or
-  result = 32767.0 or
-  result = 65535.0 or
+private QlBuiltins::BigInt wideningUpperBounds(ArithmeticType t) {
+  result = -2.toBigInt() or
+  result = -1.toBigInt() or
+  result = 0.toBigInt() or
+  result = 1.toBigInt() or
+  result = 2.toBigInt() or
+  result = 7.toBigInt() or
+  result = 15.toBigInt() or
+  result = 127.toBigInt() or
+  result = 255.toBigInt() or
+  result = 32767.toBigInt() or
+  result = 65535.toBigInt() or
   result = typeUpperBound(t) or
-  result = 1.0 / 0.0 // +Inf
+  result = infinityAsBigInt() // +Inf
 }
 
 /**
@@ -165,19 +165,24 @@ float safeFloor(float v) {
 
 /** A `MulExpr` where exactly one operand is constant. */
 private class MulByConstantExpr extends MulExpr {
-  float constant;
+  float floatConstant;
+  QlBuiltins::BigInt bigIntConstant;
   Expr operand;
 
   MulByConstantExpr() {
     exists(Expr constantExpr |
       this.hasOperands(constantExpr, operand) and
-      constant = getValue(constantExpr.getFullyConverted()).toFloat() and
+      floatConstant = getValue(constantExpr.getFullyConverted()).toFloat() and
+      bigIntConstant = parseAsBigInt(getValue(constantExpr.getFullyConverted())) and
       not exists(getValue(operand.getFullyConverted()).toFloat())
     )
   }
 
   /** Gets the value of the constant operand. */
-  float getConstant() { result = constant }
+  float getFloatConstant() { result = floatConstant }
+
+  /** Gets the value of the constant operand. */
+  QlBuiltins::BigInt getBigIntConstant() { result = bigIntConstant }
 
   /** Gets the non-constant operand. */
   Expr getOperand() { result = operand }
@@ -198,10 +203,10 @@ private class UnsignedMulExpr extends MulExpr {
  * This is typically `"-1"`, but this is not guaranteed to be the case on all
  * systems.
  */
-private int getEofValue() {
+private QlBuiltins::BigInt getEofValue() {
   exists(MacroInvocation mi |
     mi.getMacroName() = "EOF" and
-    result = unique( | | mi.getExpr().getValue().toInt())
+    result = unique( | | mi.getExpr().getValue().toBigInt())
   )
 }
 
@@ -227,48 +232,58 @@ private class AnalyzableCallToGetc extends CallToGetc {
  * Holds if `expr` is effectively a multiplication of `operand` with the
  * positive constant `positive`.
  */
-private predicate effectivelyMultipliesByPositive(Expr expr, Expr operand, float positive) {
+private predicate effectivelyMultipliesByPositive(
+  Expr expr, Expr operand, QlBuiltins::BigInt positive
+) {
   operand = expr.(MulByConstantExpr).getOperand() and
-  positive = expr.(MulByConstantExpr).getConstant() and
-  positive >= 0.0 // includes positive zero
+  positive = expr.(MulByConstantExpr).getBigIntConstant() and
+  expr.(MulByConstantExpr).getFloatConstant() >= 0.0 // includes positive zero
   or
   operand = expr.(UnaryPlusExpr).getOperand() and
-  positive = 1.0
+  positive = 1.toBigInt()
   or
   operand = expr.(CommaExpr).getRightOperand() and
-  positive = 1.0
+  positive = 1.toBigInt()
   or
   operand = expr.(StmtExpr).getResultExpr() and
-  positive = 1.0
+  positive = 1.toBigInt()
 }
 
 /**
  * Holds if `expr` is effectively a multiplication of `operand` with the
  * negative constant `negative`.
  */
-private predicate effectivelyMultipliesByNegative(Expr expr, Expr operand, float negative) {
+private predicate effectivelyMultipliesByNegative(
+  Expr expr, Expr operand, QlBuiltins::BigInt negative
+) {
   operand = expr.(MulByConstantExpr).getOperand() and
-  negative = expr.(MulByConstantExpr).getConstant() and
-  negative < 0.0 // includes negative zero
+  negative = expr.(MulByConstantExpr).getBigIntConstant() and
+  expr.(MulByConstantExpr).getFloatConstant() < 0.0 // includes negative zero
   or
   operand = expr.(UnaryMinusExpr).getOperand() and
-  negative = -1.0
+  negative = -1.toBigInt()
 }
 
 private class AssignMulByConstantExpr extends AssignMulExpr {
-  float constant;
+  float floatConstant;
+  QlBuiltins::BigInt bigIntConstant;
 
-  AssignMulByConstantExpr() { constant = getValue(this.getRValue().getFullyConverted()).toFloat() }
+  AssignMulByConstantExpr() {
+    floatConstant = getValue(this.getRValue().getFullyConverted()).toFloat() and
+    bigIntConstant = parseAsBigInt(getValue(this.getRValue().getFullyConverted()))
+  }
+
+  float getFloatConstant() { result = floatConstant }
 
-  float getConstant() { result = constant }
+  QlBuiltins::BigInt getBigIntConstant() { result = bigIntConstant }
 }
 
 private class AssignMulByPositiveConstantExpr extends AssignMulByConstantExpr {
-  AssignMulByPositiveConstantExpr() { constant >= 0.0 }
+  AssignMulByPositiveConstantExpr() { floatConstant >= 0.0 }
 }
 
 private class AssignMulByNegativeConstantExpr extends AssignMulByConstantExpr {
-  AssignMulByNegativeConstantExpr() { constant < 0.0 }
+  AssignMulByNegativeConstantExpr() { floatConstant < 0.0 }
 }
 
 private class UnsignedAssignMulExpr extends AssignMulExpr {
@@ -571,55 +586,6 @@ private predicate analyzableDef(RangeSsaDefinition def, StackVariable v) {
   def.(SimpleRangeAnalysisDefinition).hasRangeInformationFor(v)
 }
 
-/**
- * Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
- * needed on the lesser side of a floating-point comparison or on both sides of
- * a floating point equality because QL does not follow IEEE in floating-point
- * comparisons but instead defines -0.0 to be less than and distinct from 0.0.
- */
-bindingset[x]
-private float normalizeFloatUp(float x) { result = x + 0.0 }
-
-/**
- * Computes `x + y`, rounded towards +Inf. This is the general case where both
- * `x` and `y` may be large numbers.
- */
-bindingset[x, y]
-private float addRoundingUp(float x, float y) {
-  if normalizeFloatUp((x + y) - x) < y or normalizeFloatUp((x + y) - y) < x
-  then result = (x + y).nextUp()
-  else result = (x + y)
-}
-
-/**
- * Computes `x + y`, rounded towards -Inf. This is the general case where both
- * `x` and `y` may be large numbers.
- */
-bindingset[x, y]
-private float addRoundingDown(float x, float y) {
-  if (x + y) - x > normalizeFloatUp(y) or (x + y) - y > normalizeFloatUp(x)
-  then result = (x + y).nextDown()
-  else result = (x + y)
-}
-
-/**
- * Computes `x + small`, rounded towards +Inf, where `small` is a small
- * constant.
- */
-bindingset[x, small]
-private float addRoundingUpSmall(float x, float small) {
-  if (x + small) - x < small then result = (x + small).nextUp() else result = (x + small)
-}
-
-/**
- * Computes `x + small`, rounded towards -Inf, where `small` is a small
- * constant.
- */
-bindingset[x, small]
-private float addRoundingDownSmall(float x, float small) {
-  if (x + small) - x > small then result = (x + small).nextDown() else result = (x + small)
-}
-
 private predicate lowerBoundableExpr(Expr expr) {
   analyzableExpr(expr) and
   getUpperBoundsImpl(expr) <= exprMaxVal(expr) and
@@ -643,22 +609,22 @@ private predicate lowerBoundableExpr(Expr expr) {
  * Note: most callers should use `getFullyConvertedLowerBounds` rather than
  * this predicate.
  */
-private float getTruncatedLowerBounds(Expr expr) {
+private QlBuiltins::BigInt getTruncatedLowerBounds(Expr expr) {
   // If the expression evaluates to a constant, then there is no
   // need to call getLowerBoundsImpl.
   analyzableExpr(expr) and
-  result = getValue(expr).toFloat()
+  result = parseAsBigInt(getValue(expr))
   or
   // Some of the bounds computed by getLowerBoundsImpl might
   // overflow, so we replace invalid bounds with exprMinVal.
-  exists(float newLB | newLB = normalizeFloatUp(getLowerBoundsImpl(expr)) |
+  exists(QlBuiltins::BigInt newLB | newLB = getLowerBoundsImpl(expr) |
     if exprMinVal(expr) <= newLB and newLB <= exprMaxVal(expr)
     then
       // Apply widening where we might get a combinatorial explosion.
       if isRecursiveBinary(expr)
       then
         result =
-          max(float widenLB |
+          max(QlBuiltins::BigInt widenLB |
             widenLB = wideningLowerBounds(expr.getUnspecifiedType()) and
             not widenLB > newLB
           )
@@ -671,7 +637,7 @@ private float getTruncatedLowerBounds(Expr expr) {
   // lower bound is exprMinVal.
   analyzableExpr(expr) and
   exprMightOverflowPositively(expr) and
-  not result = getValue(expr).toFloat() and
+  not result = parseAsBigInt(getValue(expr)) and
   result = exprMinVal(expr)
   or
   // The expression is not analyzable, so its lower bound is
@@ -699,25 +665,25 @@ private float getTruncatedLowerBounds(Expr expr) {
  * Note: most callers should use `getFullyConvertedUpperBounds` rather than
  * this predicate.
  */
-private float getTruncatedUpperBounds(Expr expr) {
+private QlBuiltins::BigInt getTruncatedUpperBounds(Expr expr) {
   if analyzableExpr(expr)
   then
     // If the expression evaluates to a constant, then there is no
     // need to call getUpperBoundsImpl.
-    if exists(getValue(expr).toFloat())
-    then result = getValue(expr).toFloat()
+    if exists(parseAsBigInt(getValue(expr)))
+    then result = parseAsBigInt(getValue(expr))
     else (
       // Some of the bounds computed by `getUpperBoundsImpl`
       // might overflow, so we replace invalid bounds with
       // `exprMaxVal`.
-      exists(float newUB | newUB = normalizeFloatUp(getUpperBoundsImpl(expr)) |
+      exists(QlBuiltins::BigInt newUB | newUB = getUpperBoundsImpl(expr) |
         if exprMinVal(expr) <= newUB and newUB <= exprMaxVal(expr)
         then
           // Apply widening where we might get a combinatorial explosion.
           if isRecursiveBinary(expr)
           then
             result =
-              min(float widenUB |
+              min(QlBuiltins::BigInt widenUB |
                 widenUB = wideningUpperBounds(expr.getUnspecifiedType()) and
                 not widenUB < newUB
               )
@@ -739,15 +705,15 @@ private float getTruncatedUpperBounds(Expr expr) {
 }
 
 /** Only to be called by `getTruncatedLowerBounds`. */
-private float getLowerBoundsImpl(Expr expr) {
+private QlBuiltins::BigInt getLowerBoundsImpl(Expr expr) {
   (
-    exists(Expr operand, float operandLow, float positive |
+    exists(Expr operand, QlBuiltins::BigInt operandLow, QlBuiltins::BigInt positive |
       effectivelyMultipliesByPositive(expr, operand, positive) and
       operandLow = getFullyConvertedLowerBounds(operand) and
       result = positive * operandLow
     )
     or
-    exists(Expr operand, float operandHigh, float negative |
+    exists(Expr operand, QlBuiltins::BigInt operandHigh, QlBuiltins::BigInt negative |
       effectivelyMultipliesByNegative(expr, operand, negative) and
       operandHigh = getFullyConvertedUpperBounds(operand) and
       result = negative * operandHigh
@@ -766,7 +732,7 @@ private float getLowerBoundsImpl(Expr expr) {
       //
       //    max (minimum{X}, minimum{Y})
       //  = minimum { max(x,y) | x in X, y in Y }
-      exists(float x, float y |
+      exists(QlBuiltins::BigInt x, QlBuiltins::BigInt y |
         x = getFullyConvertedLowerBounds(maxExpr.getLeftOperand()) and
         y = getFullyConvertedLowerBounds(maxExpr.getRightOperand()) and
         if x >= y then result = x else result = y
@@ -778,7 +744,7 @@ private float getLowerBoundsImpl(Expr expr) {
       expr = condExpr and
       // Use `boolConversionUpperBound` to determine whether the condition
       // might evaluate to `true`.
-      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
+      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1.toBigInt() and
       result = getFullyConvertedLowerBounds(condExpr.getThen())
     )
     or
@@ -787,25 +753,25 @@ private float getLowerBoundsImpl(Expr expr) {
       expr = condExpr and
       // Use `boolConversionLowerBound` to determine whether the condition
       // might evaluate to `false`.
-      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
+      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0.toBigInt() and
       result = getFullyConvertedLowerBounds(condExpr.getElse())
     )
     or
-    exists(AddExpr addExpr, float xLow, float yLow |
+    exists(AddExpr addExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yLow |
       expr = addExpr and
       xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and
       yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and
-      result = addRoundingDown(xLow, yLow)
+      result = xLow + yLow
     )
     or
-    exists(SubExpr subExpr, float xLow, float yHigh |
+    exists(SubExpr subExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yHigh |
       expr = subExpr and
       xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and
       yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
-      result = addRoundingDown(xLow, -yHigh)
+      result = xLow - yHigh
     )
     or
-    exists(UnsignedMulExpr mulExpr, float xLow, float yLow |
+    exists(UnsignedMulExpr mulExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yLow |
       expr = mulExpr and
       xLow = getFullyConvertedLowerBounds(mulExpr.getLeftOperand()) and
       yLow = getFullyConvertedLowerBounds(mulExpr.getRightOperand()) and
@@ -817,49 +783,49 @@ private float getLowerBoundsImpl(Expr expr) {
       result = getFullyConvertedLowerBounds(assign.getRValue())
     )
     or
-    exists(AssignAddExpr addExpr, float xLow, float yLow |
+    exists(AssignAddExpr addExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yLow |
       expr = addExpr and
       xLow = getFullyConvertedLowerBounds(addExpr.getLValue()) and
       yLow = getFullyConvertedLowerBounds(addExpr.getRValue()) and
-      result = addRoundingDown(xLow, yLow)
+      result = xLow + yLow
     )
     or
-    exists(AssignSubExpr subExpr, float xLow, float yHigh |
+    exists(AssignSubExpr subExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yHigh |
       expr = subExpr and
       xLow = getFullyConvertedLowerBounds(subExpr.getLValue()) and
       yHigh = getFullyConvertedUpperBounds(subExpr.getRValue()) and
-      result = addRoundingDown(xLow, -yHigh)
+      result = xLow - yHigh
     )
     or
-    exists(UnsignedAssignMulExpr mulExpr, float xLow, float yLow |
+    exists(UnsignedAssignMulExpr mulExpr, QlBuiltins::BigInt xLow, QlBuiltins::BigInt yLow |
       expr = mulExpr and
       xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
       yLow = getFullyConvertedLowerBounds(mulExpr.getRValue()) and
       result = xLow * yLow
     )
     or
-    exists(AssignMulByPositiveConstantExpr mulExpr, float xLow |
+    exists(AssignMulByPositiveConstantExpr mulExpr, QlBuiltins::BigInt xLow |
       expr = mulExpr and
       xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
-      result = xLow * mulExpr.getConstant()
+      result = xLow * mulExpr.getBigIntConstant()
     )
     or
-    exists(AssignMulByNegativeConstantExpr mulExpr, float xHigh |
+    exists(AssignMulByNegativeConstantExpr mulExpr, QlBuiltins::BigInt xHigh |
       expr = mulExpr and
       xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
-      result = xHigh * mulExpr.getConstant()
+      result = xHigh * mulExpr.getBigIntConstant()
     )
     or
-    exists(PrefixIncrExpr incrExpr, float xLow |
+    exists(PrefixIncrExpr incrExpr, QlBuiltins::BigInt xLow |
       expr = incrExpr and
       xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
-      result = xLow + 1
+      result = xLow + 1.toBigInt()
     )
     or
-    exists(PrefixDecrExpr decrExpr, float xLow |
+    exists(PrefixDecrExpr decrExpr, QlBuiltins::BigInt xLow |
       expr = decrExpr and
       xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and
-      result = addRoundingDownSmall(xLow, -1)
+      result = xLow - 1.toBigInt()
     )
     or
     // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their
@@ -877,19 +843,21 @@ private float getLowerBoundsImpl(Expr expr) {
     or
     exists(RemExpr remExpr | expr = remExpr |
       // If both inputs are positive then the lower bound is zero.
-      result = 0
+      result = 0.toBigInt()
       or
       // If either input could be negative then the output could be
       // negative. If so, the lower bound of `x%y` is `-abs(y) + 1`, which is
       // equal to `min(-y + 1,y - 1)`.
-      exists(float childLB |
+      exists(QlBuiltins::BigInt childLB |
         childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
-        not childLB >= 0
+        not childLB >= 0.toBigInt()
       |
-        result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
+        result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1.toBigInt()
         or
-        exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) |
-          result = -rhsUB + 1
+        exists(QlBuiltins::BigInt rhsUB |
+          rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
+        |
+          result = -rhsUB + 1.toBigInt()
         )
       )
     )
@@ -921,15 +889,15 @@ private float getLowerBoundsImpl(Expr expr) {
     // unsigned `&` (tighter bounds may exist)
     exists(UnsignedBitwiseAndExpr andExpr |
       andExpr = expr and
-      result = 0.0
+      result = 0.toBigInt()
     )
     or
     // `>>` by a constant
-    exists(RShiftExpr rsExpr, float left, int right |
+    exists(RShiftExpr rsExpr, QlBuiltins::BigInt left, int right |
       rsExpr = expr and
       left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and
       right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
-      result = safeFloor(left / 2.pow(right))
+      result = left / 2.toBigInt().pow(right)
     )
     // Not explicitly modeled by a SimpleRangeAnalysisExpr
   ) and
@@ -943,15 +911,15 @@ private float getLowerBoundsImpl(Expr expr) {
 }
 
 /** Only to be called by `getTruncatedUpperBounds`. */
-private float getUpperBoundsImpl(Expr expr) {
+private QlBuiltins::BigInt getUpperBoundsImpl(Expr expr) {
   (
-    exists(Expr operand, float operandHigh, float positive |
+    exists(Expr operand, QlBuiltins::BigInt operandHigh, QlBuiltins::BigInt positive |
       effectivelyMultipliesByPositive(expr, operand, positive) and
       operandHigh = getFullyConvertedUpperBounds(operand) and
       result = positive * operandHigh
     )
     or
-    exists(Expr operand, float operandLow, float negative |
+    exists(Expr operand, QlBuiltins::BigInt operandLow, QlBuiltins::BigInt negative |
       effectivelyMultipliesByNegative(expr, operand, negative) and
       operandLow = getFullyConvertedLowerBounds(operand) and
       result = negative * operandLow
@@ -970,7 +938,7 @@ private float getUpperBoundsImpl(Expr expr) {
       //
       //    min (maximum{X}, maximum{Y})
       //  = maximum { min(x,y) | x in X, y in Y }
-      exists(float x, float y |
+      exists(QlBuiltins::BigInt x, QlBuiltins::BigInt y |
         x = getFullyConvertedUpperBounds(minExpr.getLeftOperand()) and
         y = getFullyConvertedUpperBounds(minExpr.getRightOperand()) and
         if x <= y then result = x else result = y
@@ -982,7 +950,7 @@ private float getUpperBoundsImpl(Expr expr) {
       expr = condExpr and
       // Use `boolConversionUpperBound` to determine whether the condition
       // might evaluate to `true`.
-      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
+      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1.toBigInt() and
       result = getFullyConvertedUpperBounds(condExpr.getThen())
     )
     or
@@ -991,25 +959,25 @@ private float getUpperBoundsImpl(Expr expr) {
       expr = condExpr and
       // Use `boolConversionLowerBound` to determine whether the condition
       // might evaluate to `false`.
-      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
+      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0.toBigInt() and
       result = getFullyConvertedUpperBounds(condExpr.getElse())
     )
     or
-    exists(AddExpr addExpr, float xHigh, float yHigh |
+    exists(AddExpr addExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yHigh |
       expr = addExpr and
       xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and
       yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and
-      result = addRoundingUp(xHigh, yHigh)
+      result = xHigh + yHigh
     )
     or
-    exists(SubExpr subExpr, float xHigh, float yLow |
+    exists(SubExpr subExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yLow |
       expr = subExpr and
       xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and
       yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
-      result = addRoundingUp(xHigh, -yLow)
+      result = xHigh - yLow
     )
     or
-    exists(UnsignedMulExpr mulExpr, float xHigh, float yHigh |
+    exists(UnsignedMulExpr mulExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yHigh |
       expr = mulExpr and
       xHigh = getFullyConvertedUpperBounds(mulExpr.getLeftOperand()) and
       yHigh = getFullyConvertedUpperBounds(mulExpr.getRightOperand()) and
@@ -1021,49 +989,49 @@ private float getUpperBoundsImpl(Expr expr) {
       result = getFullyConvertedUpperBounds(assign.getRValue())
     )
     or
-    exists(AssignAddExpr addExpr, float xHigh, float yHigh |
+    exists(AssignAddExpr addExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yHigh |
       expr = addExpr and
       xHigh = getFullyConvertedUpperBounds(addExpr.getLValue()) and
       yHigh = getFullyConvertedUpperBounds(addExpr.getRValue()) and
-      result = addRoundingUp(xHigh, yHigh)
+      result = xHigh + yHigh
     )
     or
-    exists(AssignSubExpr subExpr, float xHigh, float yLow |
+    exists(AssignSubExpr subExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yLow |
       expr = subExpr and
       xHigh = getFullyConvertedUpperBounds(subExpr.getLValue()) and
       yLow = getFullyConvertedLowerBounds(subExpr.getRValue()) and
-      result = addRoundingUp(xHigh, -yLow)
+      result = xHigh - yLow
     )
     or
-    exists(UnsignedAssignMulExpr mulExpr, float xHigh, float yHigh |
+    exists(UnsignedAssignMulExpr mulExpr, QlBuiltins::BigInt xHigh, QlBuiltins::BigInt yHigh |
       expr = mulExpr and
       xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
       yHigh = getFullyConvertedUpperBounds(mulExpr.getRValue()) and
       result = xHigh * yHigh
     )
     or
-    exists(AssignMulByPositiveConstantExpr mulExpr, float xHigh |
+    exists(AssignMulByPositiveConstantExpr mulExpr, QlBuiltins::BigInt xHigh |
       expr = mulExpr and
       xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
-      result = xHigh * mulExpr.getConstant()
+      result = xHigh * mulExpr.getBigIntConstant()
     )
     or
-    exists(AssignMulByNegativeConstantExpr mulExpr, float xLow |
+    exists(AssignMulByNegativeConstantExpr mulExpr, QlBuiltins::BigInt xLow |
       expr = mulExpr and
       xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
-      result = xLow * mulExpr.getConstant()
+      result = xLow * mulExpr.getBigIntConstant()
     )
     or
-    exists(PrefixIncrExpr incrExpr, float xHigh |
+    exists(PrefixIncrExpr incrExpr, QlBuiltins::BigInt xHigh |
       expr = incrExpr and
       xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
-      result = addRoundingUpSmall(xHigh, 1)
+      result = xHigh + 1.toBigInt()
     )
     or
-    exists(PrefixDecrExpr decrExpr, float xHigh |
+    exists(PrefixDecrExpr decrExpr, QlBuiltins::BigInt xHigh |
       expr = decrExpr and
       xHigh = getFullyConvertedUpperBounds(decrExpr.getOperand()) and
-      result = xHigh - 1
+      result = xHigh - 1.toBigInt()
     )
     or
     // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their operand.
@@ -1079,20 +1047,20 @@ private float getUpperBoundsImpl(Expr expr) {
       result = getFullyConvertedUpperBounds(decrExpr.getOperand())
     )
     or
-    exists(RemExpr remExpr, float rhsUB |
+    exists(RemExpr remExpr, QlBuiltins::BigInt rhsUB |
       expr = remExpr and
       rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
     |
-      result = rhsUB - 1
+      result = rhsUB - 1.toBigInt()
       or
       // If the right hand side could be negative then we need to take its
       // absolute value. Since `abs(x) = max(-x,x)` this is equivalent to
       // adding `-rhsLB` to the set of upper bounds.
-      exists(float rhsLB |
+      exists(QlBuiltins::BigInt rhsLB |
         rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
-        not rhsLB >= 0
+        not rhsLB >= 0.toBigInt()
       |
-        result = -rhsLB + 1
+        result = 1.toBigInt() - rhsLB
       )
     )
     or
@@ -1121,7 +1089,7 @@ private float getUpperBoundsImpl(Expr expr) {
     )
     or
     // unsigned `&` (tighter bounds may exist)
-    exists(UnsignedBitwiseAndExpr andExpr, float left, float right |
+    exists(UnsignedBitwiseAndExpr andExpr, QlBuiltins::BigInt left, QlBuiltins::BigInt right |
       andExpr = expr and
       left = getFullyConvertedUpperBounds(andExpr.getLeftOperand()) and
       right = getFullyConvertedUpperBounds(andExpr.getRightOperand()) and
@@ -1129,11 +1097,11 @@ private float getUpperBoundsImpl(Expr expr) {
     )
     or
     // `>>` by a constant
-    exists(RShiftExpr rsExpr, float left, int right |
+    exists(RShiftExpr rsExpr, QlBuiltins::BigInt left, int right |
       rsExpr = expr and
       left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and
       right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
-      result = safeFloor(left / 2.pow(right))
+      result = left / 2.toBigInt().pow(right)
     )
     // Not explicitly modeled by a SimpleRangeAnalysisExpr
   ) and
@@ -1170,55 +1138,55 @@ private predicate exprIsUsedAsBool(Expr expr) {
  * Gets the lower bound of the conversion `(bool)expr`. If we can prove that
  * the value of `expr` is never 0 then `lb = 1`. Otherwise `lb = 0`.
  */
-private float boolConversionLowerBound(Expr expr) {
+private QlBuiltins::BigInt boolConversionLowerBound(Expr expr) {
   // Case 1: if the range for `expr` includes the value 0,
   // then `result = 0`.
   exprIsUsedAsBool(expr) and
-  exists(float lb | lb = getTruncatedLowerBounds(expr) and not lb > 0) and
-  exists(float ub | ub = getTruncatedUpperBounds(expr) and not ub < 0) and
-  result = 0
+  exists(QlBuiltins::BigInt lb | lb = getTruncatedLowerBounds(expr) and not lb > 0.toBigInt()) and
+  exists(QlBuiltins::BigInt ub | ub = getTruncatedUpperBounds(expr) and not ub < 0.toBigInt()) and
+  result = 0.toBigInt()
   or
   // Case 2a: if the range for `expr` does not include the value 0,
   // then `result = 1`.
-  exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) > 0 and result = 1
+  exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) > 0.toBigInt() and result = 1.toBigInt()
   or
   // Case 2b: if the range for `expr` does not include the value 0,
   // then `result = 1`.
-  exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) < 0 and result = 1
+  exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) < 0.toBigInt() and result = 1.toBigInt()
   or
   // Case 3: the type of `expr` is not arithmetic. For example, it might
   // be a pointer.
-  exprIsUsedAsBool(expr) and not exists(exprMinVal(expr)) and result = 0
+  exprIsUsedAsBool(expr) and not exists(exprMinVal(expr)) and result = 0.toBigInt()
 }
 
 /**
  * Gets the upper bound of the conversion `(bool)expr`. If we can prove that
  * the value of `expr` is always 0 then `ub = 0`. Otherwise `ub = 1`.
  */
-private float boolConversionUpperBound(Expr expr) {
+private QlBuiltins::BigInt boolConversionUpperBound(Expr expr) {
   // Case 1a: if the upper bound of the operand is <= 0, then the upper
   // bound might be 0.
-  exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) <= 0 and result = 0
+  exprIsUsedAsBool(expr) and getTruncatedUpperBounds(expr) <= 0.toBigInt() and result = 0.toBigInt()
   or
   // Case 1b: if the upper bound of the operand is not <= 0, then the upper
   // bound is 1.
   exprIsUsedAsBool(expr) and
-  exists(float ub | ub = getTruncatedUpperBounds(expr) and not ub <= 0) and
-  result = 1
+  exists(QlBuiltins::BigInt ub | ub = getTruncatedUpperBounds(expr) and not ub <= 0.toBigInt()) and
+  result = 1.toBigInt()
   or
   // Case 2a: if the lower bound of the operand is >= 0, then the upper
   // bound might be 0.
-  exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) >= 0 and result = 0
+  exprIsUsedAsBool(expr) and getTruncatedLowerBounds(expr) >= 0.toBigInt() and result = 0.toBigInt()
   or
   // Case 2b: if the lower bound of the operand is not >= 0, then the upper
   // bound is 1.
   exprIsUsedAsBool(expr) and
-  exists(float lb | lb = getTruncatedLowerBounds(expr) and not lb >= 0) and
-  result = 1
+  exists(QlBuiltins::BigInt lb | lb = getTruncatedLowerBounds(expr) and not lb >= 0.toBigInt()) and
+  result = 1.toBigInt()
   or
   // Case 3: the type of `expr` is not arithmetic. For example, it might
   // be a pointer.
-  exprIsUsedAsBool(expr) and not exists(exprMaxVal(expr)) and result = 1
+  exprIsUsedAsBool(expr) and not exists(exprMaxVal(expr)) and result = 1.toBigInt()
 }
 
 /**
@@ -1235,8 +1203,11 @@ private float boolConversionUpperBound(Expr expr) {
  * In this example, the lower bound of x is 0, but we can
  * use the guard to deduce that the lower bound is 2 inside the block.
  */
-private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
-  exists(VariableAccess access, Expr guard, boolean branch, float defLB, float guardLB |
+private QlBuiltins::BigInt getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
+  exists(
+    VariableAccess access, Expr guard, boolean branch, QlBuiltins::BigInt defLB,
+    QlBuiltins::BigInt guardLB
+  |
     phi.isGuardPhi(v, access, guard, branch) and
     lowerBoundFromGuard(guard, access, guardLB, branch) and
     defLB = getFullyConvertedLowerBounds(access)
@@ -1245,10 +1216,10 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
     if guardLB > defLB then result = guardLB else result = defLB
   )
   or
-  exists(VariableAccess access, float neConstant, float lower |
+  exists(VariableAccess access, QlBuiltins::BigInt neConstant, QlBuiltins::BigInt lower |
     isNEPhi(v, phi, access, neConstant) and
     lower = getTruncatedLowerBounds(access) and
-    if lower = neConstant then result = lower + 1 else result = lower
+    if lower = neConstant then result = lower + 1.toBigInt() else result = lower
   )
   or
   exists(VariableAccess access |
@@ -1260,8 +1231,11 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
 }
 
 /** See comment for `getPhiLowerBounds`, above. */
-private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
-  exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB |
+private QlBuiltins::BigInt getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
+  exists(
+    VariableAccess access, Expr guard, boolean branch, QlBuiltins::BigInt defUB,
+    QlBuiltins::BigInt guardUB
+  |
     phi.isGuardPhi(v, access, guard, branch) and
     upperBoundFromGuard(guard, access, guardUB, branch) and
     defUB = getFullyConvertedUpperBounds(access)
@@ -1270,10 +1244,10 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
     if guardUB < defUB then result = guardUB else result = defUB
   )
   or
-  exists(VariableAccess access, float neConstant, float upper |
+  exists(VariableAccess access, QlBuiltins::BigInt neConstant, QlBuiltins::BigInt upper |
     isNEPhi(v, phi, access, neConstant) and
     upper = getTruncatedUpperBounds(access) and
-    if upper = neConstant then result = upper - 1 else result = upper
+    if upper = neConstant then result = upper - 1.toBigInt() else result = upper
   )
   or
   exists(VariableAccess access |
@@ -1285,7 +1259,7 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
 }
 
 /** Only to be called by `getDefLowerBounds`. */
-private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
+private QlBuiltins::BigInt getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
   // Definitions with a defining value.
   exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedLowerBounds(expr))
   or
@@ -1296,18 +1270,18 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
     result = getTruncatedLowerBounds(assignOp)
   )
   or
-  exists(IncrementOperation incr, float newLB |
+  exists(IncrementOperation incr, QlBuiltins::BigInt newLB |
     def = incr and
     incr.getOperand() = v.getAnAccess() and
     newLB = getFullyConvertedLowerBounds(incr.getOperand()) and
-    result = newLB + 1
+    result = newLB + 1.toBigInt()
   )
   or
-  exists(DecrementOperation decr, float newLB |
+  exists(DecrementOperation decr, QlBuiltins::BigInt newLB |
     def = decr and
     decr.getOperand() = v.getAnAccess() and
     newLB = getFullyConvertedLowerBounds(decr.getOperand()) and
-    result = addRoundingDownSmall(newLB, -1)
+    result = newLB - 1.toBigInt()
   )
   or
   // Phi nodes.
@@ -1321,7 +1295,7 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
 }
 
 /** Only to be called by `getDefUpperBounds`. */
-private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
+private QlBuiltins::BigInt getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
   // Definitions with a defining value.
   exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedUpperBounds(expr))
   or
@@ -1332,18 +1306,18 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
     result = getTruncatedUpperBounds(assignOp)
   )
   or
-  exists(IncrementOperation incr, float newUB |
+  exists(IncrementOperation incr, QlBuiltins::BigInt newUB |
     def = incr and
     incr.getOperand() = v.getAnAccess() and
     newUB = getFullyConvertedUpperBounds(incr.getOperand()) and
-    result = addRoundingUpSmall(newUB, 1)
+    result = newUB + 1.toBigInt()
   )
   or
-  exists(DecrementOperation decr, float newUB |
+  exists(DecrementOperation decr, QlBuiltins::BigInt newUB |
     def = decr and
     decr.getOperand() = v.getAnAccess() and
     newUB = getFullyConvertedUpperBounds(decr.getOperand()) and
-    result = newUB - 1
+    result = newUB - 1.toBigInt()
   )
   or
   // Phi nodes.
@@ -1361,7 +1335,9 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
  * unanalyzable definitions (such as function parameters) and make their
  * bounds unknown.
  */
-private predicate unanalyzableDefBounds(RangeSsaDefinition def, StackVariable v, float lb, float ub) {
+private predicate unanalyzableDefBounds(
+  RangeSsaDefinition def, StackVariable v, QlBuiltins::BigInt lb, QlBuiltins::BigInt ub
+) {
   v = def.getAVariable() and
   not analyzableDef(def, v) and
   lb = varMinVal(v) and
@@ -1393,8 +1369,10 @@ predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
  * predicate uses the bounds information for `r` to compute a lower bound
  * for `v`.
  */
-private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, boolean branch) {
-  exists(float childLB, RelationStrictness strictness |
+private predicate lowerBoundFromGuard(
+  Expr guard, VariableAccess v, QlBuiltins::BigInt lb, boolean branch
+) {
+  exists(QlBuiltins::BigInt childLB, RelationStrictness strictness |
     boundFromGuard(guard, v, childLB, true, strictness, branch)
   |
     if nonNanGuardedVariable(guard, v, branch)
@@ -1403,7 +1381,7 @@ private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, bo
         strictness = Nonstrict() or
         not getVariableRangeType(v.getTarget()) instanceof IntegralType
       then lb = childLB
-      else lb = childLB + 1
+      else lb = childLB + 1.toBigInt()
     else lb = varMinVal(v.getTarget())
   )
 }
@@ -1413,8 +1391,10 @@ private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, bo
  * predicate uses the bounds information for `r` to compute a upper bound
  * for `v`.
  */
-private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, boolean branch) {
-  exists(float childUB, RelationStrictness strictness |
+private predicate upperBoundFromGuard(
+  Expr guard, VariableAccess v, QlBuiltins::BigInt ub, boolean branch
+) {
+  exists(QlBuiltins::BigInt childUB, RelationStrictness strictness |
     boundFromGuard(guard, v, childUB, false, strictness, branch)
   |
     if nonNanGuardedVariable(guard, v, branch)
@@ -1423,7 +1403,7 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
         strictness = Nonstrict() or
         not getVariableRangeType(v.getTarget()) instanceof IntegralType
       then ub = childUB
-      else ub = childUB - 1
+      else ub = childUB - 1.toBigInt()
     else ub = varMaxVal(v.getTarget())
   )
 }
@@ -1433,25 +1413,25 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
  * `linearBoundFromGuard`.
  */
 private predicate boundFromGuard(
-  Expr guard, VariableAccess v, float boundValue, boolean isLowerBound,
+  Expr guard, VariableAccess v, QlBuiltins::BigInt boundValue, boolean isLowerBound,
   RelationStrictness strictness, boolean branch
 ) {
-  exists(float p, float q, float r, boolean isLB |
+  exists(QlBuiltins::BigInt p, QlBuiltins::BigInt q, QlBuiltins::BigInt r, boolean isLB |
     linearBoundFromGuard(guard, v, p, q, r, isLB, strictness, branch) and
     boundValue = (r - q) / p
   |
     // If the multiplier is negative then the direction of the comparison
     // needs to be flipped.
-    p > 0 and isLowerBound = isLB
+    p > 0.toBigInt() and isLowerBound = isLB
     or
-    p < 0 and isLowerBound = isLB.booleanNot()
+    p < 0.toBigInt() and isLowerBound = isLB.booleanNot()
   )
   or
   // When `!e` is true, we know that `0 <= e <= 0`
-  exists(float p, float q, Expr e |
+  exists(QlBuiltins::BigInt p, QlBuiltins::BigInt q, Expr e |
     linearAccess(e, v, p, q) and
     eqZeroWithNegate(guard, e, true, branch) and
-    boundValue = (0.0 - q) / p and
+    boundValue = -q / p and
     isLowerBound = [false, true] and
     strictness = Nonstrict()
   )
@@ -1463,8 +1443,8 @@ private predicate boundFromGuard(
  * lower or upper bound for `v`.
  */
 private predicate linearBoundFromGuard(
-  ComparisonOperation guard, VariableAccess v, float p, float q, float boundValue,
-  boolean isLowerBound, // Is this a lower or an upper bound?
+  ComparisonOperation guard, VariableAccess v, QlBuiltins::BigInt p, QlBuiltins::BigInt q,
+  QlBuiltins::BigInt boundValue, boolean isLowerBound, // Is this a lower or an upper bound?
   RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on?
 ) {
   // For the comparison x < RHS, we create two bounds:
@@ -1500,14 +1480,14 @@ private predicate linearBoundFromGuard(
 }
 
 /** Utility for `linearBoundFromGuard`. */
-private predicate getBounds(Expr expr, float boundValue, boolean isLowerBound) {
+private predicate getBounds(Expr expr, QlBuiltins::BigInt boundValue, boolean isLowerBound) {
   isLowerBound = true and boundValue = getFullyConvertedLowerBounds(expr)
   or
   isLowerBound = false and boundValue = getFullyConvertedUpperBounds(expr)
 }
 
 /** Utility for `linearBoundFromGuard`. */
-private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) {
+private predicate exprTypeBounds(Expr expr, QlBuiltins::BigInt boundValue, boolean isLowerBound) {
   isLowerBound = true and boundValue = exprMinVal(expr.getFullyConverted())
   or
   isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted())
@@ -1519,25 +1499,26 @@ private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBou
  * Only integral types are supported.
  */
 private predicate isNEPhi(
-  Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant
+  Variable v, RangeSsaDefinition phi, VariableAccess access, QlBuiltins::BigInt neConstant
 ) {
   exists(
-    ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q, float r
+    ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, QlBuiltins::BigInt p,
+    QlBuiltins::BigInt q, QlBuiltins::BigInt r
   |
     phi.isGuardPhi(v, access, cmp, branch) and
     eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
     v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
-    r = getValue(rExpr).toFloat() and
+    r = parseAsBigInt(getValue(rExpr)) and
     linearAccess(linearExpr, access, p, q) and
     neConstant = (r - q) / p
   )
   or
-  exists(Expr op, boolean branch, Expr linearExpr, float p, float q |
+  exists(Expr op, boolean branch, Expr linearExpr, QlBuiltins::BigInt p, QlBuiltins::BigInt q |
     phi.isGuardPhi(v, access, op, branch) and
     eqZeroWithNegate(op, linearExpr, false, branch) and
     v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise
     linearAccess(linearExpr, access, p, q) and
-    neConstant = (0.0 - q) / p
+    neConstant = -q / p
   )
 }
 
@@ -1563,7 +1544,7 @@ private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, Vari
  * An upper bound can only be found, if a guard phi node can be found, and the
  * expression has only one immediate predecessor.
  */
-private float getGuardedUpperBound(VariableAccess guardedAccess) {
+private QlBuiltins::BigInt getGuardedUpperBound(VariableAccess guardedAccess) {
   exists(
     RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard, boolean branch
   |
@@ -1577,7 +1558,7 @@ private float getGuardedUpperBound(VariableAccess guardedAccess) {
     // that there is one predecessor, albeit somewhat conservative.
     exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and
     guardedAccess = def.getAUse(v) and
-    result = max(float ub | upperBoundFromGuard(guard, guardVa, ub, branch)) and
+    result = max(QlBuiltins::BigInt ub | upperBoundFromGuard(guard, guardVa, ub, branch)) and
     not convertedExprMightOverflow(guard.getAChild+())
   )
 }
@@ -1597,10 +1578,10 @@ private module SimpleRangeAnalysisCached {
    *    `lowerBound(expr.getFullyConverted())`
    */
   cached
-  float lowerBound(Expr expr) {
+  QlBuiltins::BigInt lowerBound(Expr expr) {
     // Combine the lower bounds returned by getTruncatedLowerBounds into a
     // single minimum value.
-    result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb)
+    result = min(QlBuiltins::BigInt lb | lb = getTruncatedLowerBounds(expr) | lb)
   }
 
   /**
@@ -1616,7 +1597,7 @@ private module SimpleRangeAnalysisCached {
    *    `upperBound(expr.getFullyConverted())`
    */
   cached
-  float upperBound(Expr expr) {
+  QlBuiltins::BigInt upperBound(Expr expr) {
     // Combine the upper bounds returned by getTruncatedUpperBounds and
     // getGuardedUpperBound into a single maximum value
     result = min([max(getTruncatedUpperBounds(expr)), getGuardedUpperBound(expr)])
@@ -1776,14 +1757,14 @@ module SimpleRangeAnalysisInternal {
   /**
    * Gets the truncated lower bounds of the fully converted expression.
    */
-  float getFullyConvertedLowerBounds(Expr expr) {
+  QlBuiltins::BigInt getFullyConvertedLowerBounds(Expr expr) {
     result = getTruncatedLowerBounds(expr.getFullyConverted())
   }
 
   /**
    * Gets the truncated upper bounds of the fully converted expression.
    */
-  float getFullyConvertedUpperBounds(Expr expr) {
+  QlBuiltins::BigInt getFullyConvertedUpperBounds(Expr expr) {
     result = getTruncatedUpperBounds(expr.getFullyConverted())
   }
 
@@ -1792,8 +1773,8 @@ module SimpleRangeAnalysisInternal {
    * done by `getDefLowerBoundsImpl`, but this is where widening is applied
    * to prevent the analysis from exploding due to a recursive definition.
    */
-  float getDefLowerBounds(RangeSsaDefinition def, StackVariable v) {
-    exists(float newLB, float truncatedLB |
+  QlBuiltins::BigInt getDefLowerBounds(RangeSsaDefinition def, StackVariable v) {
+    exists(QlBuiltins::BigInt newLB, QlBuiltins::BigInt truncatedLB |
       newLB = getDefLowerBoundsImpl(def, v) and
       if varMinVal(v) <= newLB and newLB <= varMaxVal(v)
       then truncatedLB = newLB
@@ -1807,7 +1788,7 @@ module SimpleRangeAnalysisInternal {
         // down to one of a limited set of values to prevent the
         // recursion from exploding.
         result =
-          max(float widenLB |
+          max(QlBuiltins::BigInt widenLB |
             widenLB = wideningLowerBounds(getVariableRangeType(v)) and
             not widenLB > truncatedLB
           |
@@ -1822,8 +1803,8 @@ module SimpleRangeAnalysisInternal {
   }
 
   /** See comment for `getDefLowerBounds`, above. */
-  float getDefUpperBounds(RangeSsaDefinition def, StackVariable v) {
-    exists(float newUB, float truncatedUB |
+  QlBuiltins::BigInt getDefUpperBounds(RangeSsaDefinition def, StackVariable v) {
+    exists(QlBuiltins::BigInt newUB, QlBuiltins::BigInt truncatedUB |
       newUB = getDefUpperBoundsImpl(def, v) and
       if varMinVal(v) <= newUB and newUB <= varMaxVal(v)
       then truncatedUB = newUB
@@ -1837,7 +1818,7 @@ module SimpleRangeAnalysisInternal {
         // up to one of a fixed set of values to prevent the recursion
         // from exploding.
         result =
-          min(float widenUB |
+          min(QlBuiltins::BigInt widenUB |
             widenUB = wideningUpperBounds(getVariableRangeType(v)) and
             not widenUB < truncatedUB
           |
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll
index dc5e1a25f0eb..0cd5d19f5db6 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll
@@ -97,7 +97,7 @@ predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
  * due to a conversion.
  */
 predicate exprMightOverflowNegatively(Expr expr) {
-  lowerBound(expr) < exprMinVal(expr)
+  lowerBound(expr) < exprMinVal(expr).toString().toFloat()
   or
   exists(SemanticExprConfig::Expr semExpr |
     semExpr.getAst() = expr and
@@ -123,7 +123,7 @@ predicate convertedExprMightOverflowNegatively(Expr expr) {
  * due to a conversion.
  */
 predicate exprMightOverflowPositively(Expr expr) {
-  upperBound(expr) > exprMaxVal(expr)
+  upperBound(expr) > exprMaxVal(expr).toString().toFloat()
   or
   exists(SemanticExprConfig::Expr semExpr |
     semExpr.getAst() = expr and

From b7b6cd5f3eda546a4aa491af4f8d69b8760345e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Thu, 27 Jun 2024 12:44:42 +0200
Subject: [PATCH 2/6] SimpleRangeAnalysis src/: float -> BigInt

---
 cpp/ql/src/Critical/OverflowStatic.ql         | 11 ++--
 .../Likely Bugs/Arithmetic/IntMultToLong.ql   | 32 ++++++-----
 .../Arithmetic/PointlessComparison.ql         |  4 +-
 .../CWE-129/ImproperArrayIndexValidation.ql   |  2 +-
 .../CWE/CWE-190/ComparisonWithWiderType.ql    |  3 +-
 ...nsignedDifferenceExpressionComparedZero.ql | 18 +++----
 .../Likely Bugs/DerefNullResult.cpp           |  5 ++
 .../Likely Bugs/RedundantNullCheckParam.cpp   |  2 +
 .../CWE/CWE-561/FindIncorrectlyUsedSwitch.ql  | 46 ++++++++--------
 ...cErrorWhenUseBitwiseOrLogicalOperations.ql | 54 ++++++++++---------
 10 files changed, 98 insertions(+), 79 deletions(-)

diff --git a/cpp/ql/src/Critical/OverflowStatic.ql b/cpp/ql/src/Critical/OverflowStatic.ql
index 519c3f9b4015..9f471f3afc23 100644
--- a/cpp/ql/src/Critical/OverflowStatic.ql
+++ b/cpp/ql/src/Critical/OverflowStatic.ql
@@ -58,7 +58,8 @@ predicate overflowOffsetInLoop(BufferAccess bufaccess, string msg) {
     loop.limit() >= bufaccess.bufferSize() and
     loop.counter().getAnAccess() = bufaccess.getArrayOffset() and
     // Ensure that we don't have an upper bound on the array index that's less than the buffer size.
-    not upperBound(bufaccess.getArrayOffset().getFullyConverted()) < bufaccess.bufferSize() and
+    not upperBound(bufaccess.getArrayOffset().getFullyConverted()) <
+      bufaccess.bufferSize().toBigInt() and
     // The upper bounds analysis must not have been widended
     not upperBoundMayBeWidened(bufaccess.getArrayOffset().getFullyConverted()) and
     msg =
@@ -103,7 +104,7 @@ class CallWithBufferSize extends FunctionCall {
     )
   }
 
-  int statedSizeValue() {
+  QlBuiltins::BigInt statedSizeValue() {
     // `upperBound(e)` defaults to `exprMaxVal(e)` when `e` isn't analyzable. So to get a meaningful
     // result in this case we pick the minimum value obtainable from dataflow and range analysis.
     result =
@@ -111,16 +112,16 @@ class CallWithBufferSize extends FunctionCall {
           .minimum(min(Expr statedSizeSrc |
               DataFlow::localExprFlow(statedSizeSrc, this.statedSizeExpr())
             |
-              statedSizeSrc.getValue().toInt()
+              statedSizeSrc.getValue().toBigInt()
             ))
   }
 }
 
 predicate wrongBufferSize(Expr error, string msg) {
-  exists(CallWithBufferSize call, int bufsize, Variable buf, int statedSize |
+  exists(CallWithBufferSize call, int bufsize, Variable buf, QlBuiltins::BigInt statedSize |
     staticBuffer(call.buffer(), buf, bufsize) and
     statedSize = call.statedSizeValue() and
-    statedSize > bufsize and
+    statedSize > bufsize.toBigInt() and
     error = call.statedSizeExpr() and
     msg =
       "Potential buffer-overflow: '" + buf.getName() + "' has size " + bufsize.toString() + " not " +
diff --git a/cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql b/cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql
index ba7a6b58aa01..29cd160cad4f 100644
--- a/cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql	
+++ b/cpp/ql/src/Likely Bugs/Arithmetic/IntMultToLong.ql	
@@ -76,20 +76,22 @@ int getEffectiveMulOperands(MulExpr me) {
  * using SimpleRangeAnalysis.
  */
 class AnalyzableExpr extends Expr {
-  float maxValue() { result = upperBound(this.getFullyConverted()) }
+  QlBuiltins::BigInt maxValue() { result = upperBound(this.getFullyConverted()) }
 
-  float minValue() { result = lowerBound(this.getFullyConverted()) }
+  QlBuiltins::BigInt minValue() { result = lowerBound(this.getFullyConverted()) }
 }
 
 class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr {
-  override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
+  override QlBuiltins::BigInt maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
 
-  override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
+  override QlBuiltins::BigInt minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
 }
 
 class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
-  override float maxValue() {
-    exists(float x1, float y1, float x2, float y2 |
+  override QlBuiltins::BigInt maxValue() {
+    exists(
+      QlBuiltins::BigInt x1, QlBuiltins::BigInt y1, QlBuiltins::BigInt x2, QlBuiltins::BigInt y2
+    |
       x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
       x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
       y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
@@ -98,8 +100,10 @@ class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
     )
   }
 
-  override float minValue() {
-    exists(float x1, float x2, float y1, float y2 |
+  override QlBuiltins::BigInt minValue() {
+    exists(
+      QlBuiltins::BigInt x1, QlBuiltins::BigInt x2, QlBuiltins::BigInt y1, QlBuiltins::BigInt y2
+    |
       x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
       x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
       y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
@@ -110,13 +114,13 @@ class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
 }
 
 class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
-  override float maxValue() {
+  override QlBuiltins::BigInt maxValue() {
     result =
       this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() +
         this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
   }
 
-  override float minValue() {
+  override QlBuiltins::BigInt minValue() {
     result =
       this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() +
         this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
@@ -124,13 +128,13 @@ class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
 }
 
 class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
-  override float maxValue() {
+  override QlBuiltins::BigInt maxValue() {
     result =
       this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() -
         this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
   }
 
-  override float minValue() {
+  override QlBuiltins::BigInt minValue() {
     result =
       this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() -
         this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
@@ -140,7 +144,7 @@ class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
 class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
   VarAnalyzableExpr() { this.getTarget() instanceof StackVariable }
 
-  override float maxValue() {
+  override QlBuiltins::BigInt maxValue() {
     exists(SsaDefinition def, Variable v |
       def.getAUse(v) = this and
       // if there is a defining expression, use that for
@@ -152,7 +156,7 @@ class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
     )
   }
 
-  override float minValue() {
+  override QlBuiltins::BigInt minValue() {
     exists(SsaDefinition def, Variable v |
       def.getAUse(v) = this and
       if exists(def.getDefiningValue(v))
diff --git a/cpp/ql/src/Likely Bugs/Arithmetic/PointlessComparison.ql b/cpp/ql/src/Likely Bugs/Arithmetic/PointlessComparison.ql
index e2fe02be867f..991fc258d30b 100644
--- a/cpp/ql/src/Likely Bugs/Arithmetic/PointlessComparison.ql	
+++ b/cpp/ql/src/Likely Bugs/Arithmetic/PointlessComparison.ql	
@@ -26,7 +26,9 @@ import UnsignedGEZero
 // So to reduce the number of false positives, we do not report a result if
 // the comparison is in a macro expansion. Similarly for template
 // instantiations.
-from ComparisonOperation cmp, SmallSide ss, float left, float right, boolean value, string reason
+from
+  ComparisonOperation cmp, SmallSide ss, QlBuiltins::BigInt left, QlBuiltins::BigInt right,
+  boolean value, string reason
 where
   not cmp.isInMacroExpansion() and
   not cmp.isFromTemplateInstantiation(_) and
diff --git a/cpp/ql/src/Security/CWE/CWE-129/ImproperArrayIndexValidation.ql b/cpp/ql/src/Security/CWE/CWE-129/ImproperArrayIndexValidation.ql
index b5dc4d893b21..255a55390793 100644
--- a/cpp/ql/src/Security/CWE/CWE-129/ImproperArrayIndexValidation.ql
+++ b/cpp/ql/src/Security/CWE/CWE-129/ImproperArrayIndexValidation.ql
@@ -46,7 +46,7 @@ predicate guardChecks(IRGuardCondition g, Expr e, boolean branch) {
 predicate offsetIsAlwaysInBounds(ArrayExpr arrayExpr, VariableAccess offsetExpr) {
   exists(ArrayType arrayType |
     arrayType = arrayExpr.getArrayBase().getUnspecifiedType() and
-    arrayType.getArraySize() > upperBound(offsetExpr.getFullyConverted())
+    arrayType.getArraySize().toBigInt() > upperBound(offsetExpr.getFullyConverted())
   )
 }
 
diff --git a/cpp/ql/src/Security/CWE/CWE-190/ComparisonWithWiderType.ql b/cpp/ql/src/Security/CWE/CWE-190/ComparisonWithWiderType.ql
index 7d9ef88adea1..846a727c1145 100644
--- a/cpp/ql/src/Security/CWE/CWE-190/ComparisonWithWiderType.ql
+++ b/cpp/ql/src/Security/CWE/CWE-190/ComparisonWithWiderType.ql
@@ -58,7 +58,8 @@ where
     // We adjust the comparison size in the case of a signed integer type.
     // This is to exclude the sign bit from the comparison that determines if the small type's size is sufficient to hold
     // the value of the larger type determined with range analysis.
-    upperBound(conv).log2() > (getComparisonSize(small) * 8 - getComparisonSizeAdjustment(small))
+    upperBound(conv).toString().toFloat().log() / 2.log() >
+      (getComparisonSize(small) * 8 - getComparisonSizeAdjustment(small))
   ) and
   // Ignore cases where the smaller type is int or larger
   // These are still bugs, but you should need a very large string or array to
diff --git a/cpp/ql/src/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero.ql b/cpp/ql/src/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero.ql
index 02de4223c185..185eb8452780 100644
--- a/cpp/ql/src/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero.ql
+++ b/cpp/ql/src/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero.ql
@@ -62,7 +62,7 @@ Expr exprIsLeftOrLessBase(SubExpr sub) {
       // result = e - y <= e
       result = s and
       s.getLeftOperand() = e and
-      lowerBound(s.getRightOperand().getFullyConverted()) >= 0
+      lowerBound(s.getRightOperand().getFullyConverted()) >= 0.toBigInt()
     )
     or
     exists(Expr other |
@@ -73,7 +73,7 @@ Expr exprIsLeftOrLessBase(SubExpr sub) {
       // so:
       // result = e + y <= e + 0 = e
       result.(AddExpr).hasOperands(e, other) and
-      upperBound(other.getFullyConverted()) <= 0
+      upperBound(other.getFullyConverted()) <= 0.toBigInt()
     )
     or
     exists(DivExpr d |
@@ -85,7 +85,7 @@ Expr exprIsLeftOrLessBase(SubExpr sub) {
       // result = e / y <= e / 1 = e
       result = d and
       d.getLeftOperand() = e and
-      lowerBound(d.getRightOperand().getFullyConverted()) >= 1
+      lowerBound(d.getRightOperand().getFullyConverted()) >= 1.toBigInt()
     )
     or
     exists(RShiftExpr rs |
@@ -122,20 +122,20 @@ predicate exprIsSubLeftOrLess(SubExpr sub, DataFlow::Node n) {
     isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
   )
   or
-  exists(DataFlow::Node other, float p, float q |
+  exists(DataFlow::Node other, QlBuiltins::BigInt p, QlBuiltins::BigInt q |
     // linear access of `other`
     exprIsSubLeftOrLess(sub, other) and
     linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
-    p <= 1 and
-    q <= 0
+    p <= 1.toBigInt() and
+    q <= 0.toBigInt()
   )
   or
-  exists(DataFlow::Node other, float p, float q |
+  exists(DataFlow::Node other, QlBuiltins::BigInt p, QlBuiltins::BigInt q |
     // linear access of `n`
     exprIsSubLeftOrLess(sub, other) and
     linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
-    p >= 1 and
-    q >= 0
+    p >= 1.toBigInt() and
+    q >= 0.toBigInt()
   )
 }
 
diff --git a/cpp/ql/src/experimental/Likely Bugs/DerefNullResult.cpp b/cpp/ql/src/experimental/Likely Bugs/DerefNullResult.cpp
index f96d67517b75..787019bb3abf 100644
--- a/cpp/ql/src/experimental/Likely Bugs/DerefNullResult.cpp	
+++ b/cpp/ql/src/experimental/Likely Bugs/DerefNullResult.cpp	
@@ -1,3 +1,8 @@
+#define NULL nullptr
+char *malloc(int);
+void printf(const char *, ...);
+int snprintf(char *, int, const char *);
+
 char * create (int arg) {
     if (arg > 42) {
         // this function may return NULL
diff --git a/cpp/ql/src/experimental/Likely Bugs/RedundantNullCheckParam.cpp b/cpp/ql/src/experimental/Likely Bugs/RedundantNullCheckParam.cpp
index 3765d0b14d40..7b9aa815d464 100644
--- a/cpp/ql/src/experimental/Likely Bugs/RedundantNullCheckParam.cpp	
+++ b/cpp/ql/src/experimental/Likely Bugs/RedundantNullCheckParam.cpp	
@@ -1,3 +1,5 @@
+#define NULL nullptr
+
 void test(char *arg1, int *arg2) {
     if (arg1[0] == 'A') {
         if (arg2 != NULL) { //maybe redundant
diff --git a/cpp/ql/src/experimental/Security/CWE/CWE-561/FindIncorrectlyUsedSwitch.ql b/cpp/ql/src/experimental/Security/CWE/CWE-561/FindIncorrectlyUsedSwitch.ql
index a643c3e3bf08..b006d773a248 100644
--- a/cpp/ql/src/experimental/Security/CWE/CWE-561/FindIncorrectlyUsedSwitch.ql
+++ b/cpp/ql/src/experimental/Security/CWE/CWE-561/FindIncorrectlyUsedSwitch.ql
@@ -28,32 +28,32 @@ predicate isRealRange(Expr exp) {
   lowerBound(exp).toString() != "-4294967296" and
   lowerBound(exp).toString() != "-Infinity" and
   lowerBound(exp).toString() != "NaN" and
-  upperBound(exp) != 2147483647 and
-  upperBound(exp) != 268435455 and
-  upperBound(exp) != 33554431 and
-  upperBound(exp) != 8388607 and
-  upperBound(exp) != 65535 and
-  upperBound(exp) != 32767 and
-  upperBound(exp) != 255 and
-  upperBound(exp) != 127 and
-  upperBound(exp) != 63 and
-  upperBound(exp) != 31 and
-  upperBound(exp) != 15 and
-  upperBound(exp) != 7 and
-  lowerBound(exp) != -2147483648 and
-  lowerBound(exp) != -268435456 and
-  lowerBound(exp) != -33554432 and
-  lowerBound(exp) != -8388608 and
-  lowerBound(exp) != -65536 and
-  lowerBound(exp) != -32768 and
-  lowerBound(exp) != -128
+  upperBound(exp) != 2147483647.toBigInt() and
+  upperBound(exp) != 268435455.toBigInt() and
+  upperBound(exp) != 33554431.toBigInt() and
+  upperBound(exp) != 8388607.toBigInt() and
+  upperBound(exp) != 65535.toBigInt() and
+  upperBound(exp) != 32767.toBigInt() and
+  upperBound(exp) != 255.toBigInt() and
+  upperBound(exp) != 127.toBigInt() and
+  upperBound(exp) != 63.toBigInt() and
+  upperBound(exp) != 31.toBigInt() and
+  upperBound(exp) != 15.toBigInt() and
+  upperBound(exp) != 7.toBigInt() and
+  lowerBound(exp) != "-2147483648".toBigInt() and
+  lowerBound(exp) != -268435456.toBigInt() and
+  lowerBound(exp) != -33554432.toBigInt() and
+  lowerBound(exp) != -8388608.toBigInt() and
+  lowerBound(exp) != -65536.toBigInt() and
+  lowerBound(exp) != -32768.toBigInt() and
+  lowerBound(exp) != -128.toBigInt()
 }
 
 /** Holds if the range of values for the condition is less than the choices. */
 predicate isNotAllSelected(SwitchStmt swtmp) {
   not swtmp.getExpr().isConstant() and
-  exists(int i |
-    i != 0 and
+  exists(QlBuiltins::BigInt i |
+    i != 0.toBigInt() and
     (
       i = lowerBound(swtmp.getASwitchCase().getExpr()) and
       upperBound(swtmp.getExpr()) < i
@@ -70,7 +70,7 @@ predicate isNotAllSelected(SwitchStmt swtmp) {
 /** Holds if the range of values for the condition is greater than the selection. */
 predicate isConditionBig(SwitchStmt swtmp) {
   not swtmp.hasDefaultCase() and
-  not exists(int iu, int il |
+  not exists(QlBuiltins::BigInt iu, QlBuiltins::BigInt il |
     (
       iu = upperBound(swtmp.getASwitchCase().getExpr()) or
       iu = upperBound(swtmp.getASwitchCase().getEndExpr())
@@ -130,7 +130,7 @@ from SwitchStmt sw, string msg
 where
   isRealRange(sw.getExpr()) and
   lowerBound(sw.getExpr()) != upperBound(sw.getExpr()) and
-  lowerBound(sw.getExpr()) != 0 and
+  lowerBound(sw.getExpr()) != 0.toBigInt() and
   not exists(Expr cexp |
     cexp = sw.getASwitchCase().getExpr() and not isRealRange(cexp)
     or
diff --git a/cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBitwiseOrLogicalOperations.ql b/cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBitwiseOrLogicalOperations.ql
index 8bb1d0ba97bf..e0abfbefaf93 100644
--- a/cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBitwiseOrLogicalOperations.ql
+++ b/cpp/ql/src/experimental/Security/CWE/CWE-783/OperatorPrecedenceLogicErrorWhenUseBitwiseOrLogicalOperations.ql
@@ -97,24 +97,24 @@ predicate isRealRange(Expr exp) {
   lowerBound(exp).toString() != "-4294967296" and
   lowerBound(exp).toString() != "-Infinity" and
   lowerBound(exp).toString() != "NaN" and
-  upperBound(exp) != 2147483647 and
-  upperBound(exp) != 268435455 and
-  upperBound(exp) != 33554431 and
-  upperBound(exp) != 8388607 and
-  upperBound(exp) != 65535 and
-  upperBound(exp) != 32767 and
-  upperBound(exp) != 255 and
-  upperBound(exp) != 127 and
-  lowerBound(exp) != -2147483648 and
-  lowerBound(exp) != -268435456 and
-  lowerBound(exp) != -33554432 and
-  lowerBound(exp) != -8388608 and
-  lowerBound(exp) != -65536 and
-  lowerBound(exp) != -32768 and
-  lowerBound(exp) != -128
+  upperBound(exp) != 2147483647.toBigInt() and
+  upperBound(exp) != 268435455.toBigInt() and
+  upperBound(exp) != 33554431.toBigInt() and
+  upperBound(exp) != 8388607.toBigInt() and
+  upperBound(exp) != 65535.toBigInt() and
+  upperBound(exp) != 32767.toBigInt() and
+  upperBound(exp) != 255.toBigInt() and
+  upperBound(exp) != 127.toBigInt() and
+  lowerBound(exp) != "-2147483648".toBigInt() and
+  lowerBound(exp) != -268435456.toBigInt() and
+  lowerBound(exp) != -33554432.toBigInt() and
+  lowerBound(exp) != -8388608.toBigInt() and
+  lowerBound(exp) != -65536.toBigInt() and
+  lowerBound(exp) != -32768.toBigInt() and
+  lowerBound(exp) != -128.toBigInt()
   or
-  lowerBound(exp) = 0 and
-  upperBound(exp) = 1
+  lowerBound(exp) = 0.toBigInt() and
+  upperBound(exp) = 1.toBigInt()
 }
 
 /** Holds if expressions are of different size or range */
@@ -128,11 +128,15 @@ predicate isDifferentSize(Expr exp1, Expr exp2, Expr exp3) {
     isRealRange(exp2) and
     isRealRange(exp3)
   ) and
-  upperBound(exp1).maximum(upperBound(exp2)) - upperBound(exp1).minimum(upperBound(exp2)) < 16 and
-  lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) < 16 and
+  upperBound(exp1).maximum(upperBound(exp2)) - upperBound(exp1).minimum(upperBound(exp2)) <
+    16.toBigInt() and
+  lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) <
+    16.toBigInt() and
   (
-    upperBound(exp1).maximum(upperBound(exp3)) - upperBound(exp1).minimum(upperBound(exp3)) > 256 or
-    lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) > 256
+    upperBound(exp1).maximum(upperBound(exp3)) - upperBound(exp1).minimum(upperBound(exp3)) >
+      256.toBigInt() or
+    lowerBound(exp1).maximum(lowerBound(exp2)) - lowerBound(exp1).minimum(lowerBound(exp2)) >
+      256.toBigInt()
   )
 }
 
@@ -146,10 +150,10 @@ predicate isDifferentResults(
     isRealRange(exp2) and
     isRealRange(exp3)
   ) and
-  exists(int i1, int i2, int i3 |
-    i1 in [lowerBound(exp1).floor() .. upperBound(exp1).floor()] and
-    i2 in [lowerBound(exp2).floor() .. upperBound(exp2).floor()] and
-    i3 in [lowerBound(exp3).floor() .. upperBound(exp3).floor()] and
+  exists(QlBuiltins::BigInt i1, QlBuiltins::BigInt i2, QlBuiltins::BigInt i3 |
+    i1 = lowerBound(exp1) + [0 .. (upperBound(exp1) - lowerBound(exp1)).toInt()].toBigInt() and
+    i2 = lowerBound(exp2) + [0 .. (upperBound(exp2) - lowerBound(exp2)).toInt()].toBigInt() and
+    i3 = lowerBound(exp3) + [0 .. (upperBound(exp3) - lowerBound(exp3)).toInt()].toBigInt() and
     (
       op1 instanceof BitwiseOrExpr and
       op2 instanceof BitwiseAndExpr and

From 78e8de4d7331e2f80092ab07187209aba8ec012e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Thu, 27 Jun 2024 12:45:28 +0200
Subject: [PATCH 3/6] SimpleRangeAnalysis test/: float -> BigInt

---
 .../bitshift/BitShiftRange.expected           | 88 +++++++++----------
 .../rangeanalysis/bitshift/BitShiftRange.ql   |  2 +-
 .../bitwiseand/bitwiseand.expected            | 42 ++++-----
 .../rangeanalysis/bitwiseand/bitwiseand.ql    |  4 +-
 .../rangeanalysis/extended/extended.expected  | 12 +--
 .../rangeanalysis/extended/extended.ql        |  4 +-
 .../extensibility/extensibility.expected      | 18 ++--
 .../extensibility/extensibility.ql            | 24 ++---
 .../strlenliteral/StrlenLiteralRange.expected |  4 +-
 .../strlenliteral/StrlenLiteralRange.ql       |  2 +-
 .../SimpleRangeAnalysis/lowerBound.expected   |  4 +-
 .../SimpleRangeAnalysis/ternaryLower.expected | 38 ++++----
 .../SimpleRangeAnalysis/ternaryLower.ql       |  3 +-
 .../SimpleRangeAnalysis/ternaryUpper.expected | 38 ++++----
 .../SimpleRangeAnalysis/ternaryUpper.ql       |  3 +-
 .../rangeanalysis/SimpleRangeAnalysis/test.c  |  4 +-
 .../SimpleRangeAnalysis/upperBound.expected   | 40 ++++-----
 .../PointlessComparison/PointlessComparison.c |  6 +-
 .../PointlessComparison.cpp                   | 18 ++--
 .../PointlessComparison.expected              | 16 ++--
 20 files changed, 188 insertions(+), 182 deletions(-)

diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.expected
index 0a5c85dab00d..816cc25407bd 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.expected
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.expected
@@ -1,44 +1,44 @@
-| bitshift.cpp:23:3:23:9 | ... <<= ... | 0.0 | 255.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
-| bitshift.cpp:25:5:25:11 | ... <<= ... | 0.0 | 240.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
-| bitshift.cpp:29:3:29:8 | ... << ... | 0.0 | 1020.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:32:3:32:9 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:35:3:35:9 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:38:3:38:22 | ... << ... | 0.0 | 32640.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:39:3:39:22 | ... << ... | 0.0 | 32640.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:40:3:40:22 | ... << ... | 0.0 | 32640.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:43:3:43:19 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:46:3:46:22 | ... << ... | 128.0 | 128.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:49:3:49:8 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:52:5:52:10 | ... << ... | 1.0 | 128.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:57:3:57:8 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:58:3:58:9 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:59:3:59:9 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:60:3:60:22 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:61:3:61:19 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:64:3:64:19 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:67:3:67:8 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:70:5:70:10 | ... << ... | 1.0 | 128.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:75:5:75:10 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:76:5:76:10 | ... << ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:90:3:90:9 | ... >>= ... | 0.0 | 63.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
-| bitshift.cpp:92:5:92:11 | ... >>= ... | 0.0 | 15.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
-| bitshift.cpp:96:3:96:8 | ... >> ... | 0.0 | 63.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:99:3:99:9 | ... >> ... | 0.0 | 0.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:103:3:103:9 | ... >> ... | 0.0 | 0.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:106:3:106:22 | ... >> ... | 0.0 | 63.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:107:3:107:22 | ... >> ... | 0.0 | 63.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:108:3:108:22 | ... >> ... | 0.0 | 63.0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:111:3:111:19 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:114:3:114:24 | ... >> ... | 32.0 | 32.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:117:3:117:10 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:120:5:120:12 | ... >> ... | 32.0 | 128.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:126:3:126:8 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:127:3:127:9 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:128:3:128:9 | ... >> ... | -1.0 | 0.0 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:129:3:129:22 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:130:3:130:19 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:133:3:133:21 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:136:3:136:10 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:139:5:139:12 | ... >> ... | 32.0 | 128.0 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:144:5:144:10 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
-| bitshift.cpp:145:5:145:10 | ... >> ... | -2.147483648E9 | 2.147483647E9 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:23:3:23:9 | ... <<= ... | 0 | 255 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
+| bitshift.cpp:25:5:25:11 | ... <<= ... | 0 | 240 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
+| bitshift.cpp:29:3:29:8 | ... << ... | 0 | 1020 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:32:3:32:9 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:35:3:35:9 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:38:3:38:22 | ... << ... | 0 | 32640 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:39:3:39:22 | ... << ... | 0 | 32640 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:40:3:40:22 | ... << ... | 0 | 32640 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:43:3:43:19 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:46:3:46:22 | ... << ... | 128 | 128 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:49:3:49:8 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:52:5:52:10 | ... << ... | 1 | 128 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:57:3:57:8 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:58:3:58:9 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:59:3:59:9 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:60:3:60:22 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:61:3:61:19 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:64:3:64:19 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:67:3:67:8 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:70:5:70:10 | ... << ... | 1 | 128 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:75:5:75:10 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:76:5:76:10 | ... << ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:90:3:90:9 | ... >>= ... | 0 | 63 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
+| bitshift.cpp:92:5:92:11 | ... >>= ... | 0 | 15 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int |
+| bitshift.cpp:96:3:96:8 | ... >> ... | 0 | 63 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:99:3:99:9 | ... >> ... | 0 | 0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:103:3:103:9 | ... >> ... | 0 | 0 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:106:3:106:22 | ... >> ... | 0 | 63 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:107:3:107:22 | ... >> ... | 0 | 63 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:108:3:108:22 | ... >> ... | 0 | 63 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:111:3:111:19 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:114:3:114:24 | ... >> ... | 32 | 32 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:117:3:117:10 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:120:5:120:12 | ... >> ... | 32 | 128 | file://:0:0:0:0 | int | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:126:3:126:8 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:127:3:127:9 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:128:3:128:9 | ... >> ... | 0 | 0 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:129:3:129:22 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:130:3:130:19 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:133:3:133:21 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:136:3:136:10 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:139:5:139:12 | ... >> ... | 32 | 128 | file://:0:0:0:0 | int | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:144:5:144:10 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | signed char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
+| bitshift.cpp:145:5:145:10 | ... >> ... | -2147483648 | 2147483647 | file://:0:0:0:0 | signed char | file://:0:0:0:0 | unsigned char | file://:0:0:0:0 | int | file://:0:0:0:0 | int |
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.ql b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.ql
index 5429743abd5e..6f3e8abfb03f 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.ql
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitshift/BitShiftRange.ql
@@ -19,6 +19,6 @@ where
     or
     o instanceof AssignBitwiseOperation
   )
-select o, lowerBound(o), upperBound(o), getLOp(o).getUnderlyingType(),
+select o, lowerBound(o).toString(), upperBound(o).toString(), getLOp(o).getUnderlyingType(),
   getROp(o).getUnderlyingType(), getLOp(o).getFullyConverted().getUnderlyingType(),
   getROp(o).getFullyConverted().getUnderlyingType()
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.expected
index 22ad956469e4..f1674d460b9a 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.expected
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.expected
@@ -1,21 +1,21 @@
-| bitwiseand.cpp:7:3:7:8 | ... &= ... | 0.0 | 7.0 |
-| bitwiseand.cpp:15:3:15:7 | ... & ... | 0.0 | 0.0 |
-| bitwiseand.cpp:16:3:16:7 | ... & ... | 0.0 | 7.0 |
-| bitwiseand.cpp:17:3:17:20 | ... & ... | 0.0 | 7.0 |
-| bitwiseand.cpp:21:3:21:16 | ... & ... | 0.0 | 255.0 |
-| bitwiseand.cpp:28:5:28:9 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:32:5:32:9 | ... & ... | 0.0 | 100.0 |
-| bitwiseand.cpp:41:3:41:8 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:42:3:42:18 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:43:3:43:7 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:46:3:46:7 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:47:3:47:20 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:48:3:48:16 | ... & ... | 0.0 | 4.294967295E9 |
-| bitwiseand.cpp:49:3:49:25 | ... & ... | -9.223372036854776E18 | 9.223372036854776E18 |
-| bitwiseand.cpp:50:3:50:7 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:53:3:53:8 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:54:3:54:18 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:55:3:55:19 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:56:3:56:18 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:57:3:57:8 | ... & ... | -2.147483648E9 | 2.147483647E9 |
-| bitwiseand.cpp:58:3:58:19 | ... & ... | -2.147483648E9 | 2.147483647E9 |
+| bitwiseand.cpp:7:3:7:8 | ... &= ... | 0 | 7 |
+| bitwiseand.cpp:15:3:15:7 | ... & ... | 0 | 0 |
+| bitwiseand.cpp:16:3:16:7 | ... & ... | 0 | 7 |
+| bitwiseand.cpp:17:3:17:20 | ... & ... | 0 | 7 |
+| bitwiseand.cpp:21:3:21:16 | ... & ... | 0 | 255 |
+| bitwiseand.cpp:28:5:28:9 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:32:5:32:9 | ... & ... | 0 | 100 |
+| bitwiseand.cpp:41:3:41:8 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:42:3:42:18 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:43:3:43:7 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:46:3:46:7 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:47:3:47:20 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:48:3:48:16 | ... & ... | 0 | 4294967295 |
+| bitwiseand.cpp:49:3:49:25 | ... & ... | -9223372036854775808 | 9223372036854775807 |
+| bitwiseand.cpp:50:3:50:7 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:53:3:53:8 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:54:3:54:18 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:55:3:55:19 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:56:3:56:18 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:57:3:57:8 | ... & ... | -2147483648 | 2147483647 |
+| bitwiseand.cpp:58:3:58:19 | ... & ... | -2147483648 | 2147483647 |
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.ql b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.ql
index 6521e8f0f610..021f5428e19f 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.ql
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/bitwiseand/bitwiseand.ql
@@ -1,8 +1,8 @@
 import experimental.semmle.code.cpp.rangeanalysis.ExtendedRangeAnalysis
 
-from Operation expr, float lower, float upper
+from Operation expr, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper
 where
   (expr instanceof BitwiseAndExpr or expr instanceof AssignAndExpr) and
   lower = lowerBound(expr) and
   upper = upperBound(expr)
-select expr, lower, upper
+select expr, lower.toString(), upper.toString()
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.expected
index b43601c80886..e99f6e360fef 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.expected
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.expected
@@ -1,6 +1,6 @@
-| extended.cpp:4:14:4:14 | x | -2.147483648E9 | 2.147483647E9 |
-| extended.cpp:4:18:4:18 | x | -2.147483648E9 | 2.147483647E9 |
-| extended.cpp:5:3:5:6 | zero | 0.0 | 0.0 |
-| extended.cpp:7:17:7:17 | x | -2.147483648E9 | 2.147483647E9 |
-| extended.cpp:7:36:7:36 | x | -2.147483648E9 | 2.147483647E9 |
-| extended.cpp:8:3:8:9 | nonzero | -2.147483648E9 | 2.147483647E9 |
+| extended.cpp:4:14:4:14 | x | -2147483648 | 2147483647 |
+| extended.cpp:4:18:4:18 | x | -2147483648 | 2147483647 |
+| extended.cpp:5:3:5:6 | zero | 0 | 0 |
+| extended.cpp:7:17:7:17 | x | -2147483648 | 2147483647 |
+| extended.cpp:7:36:7:36 | x | -2147483648 | 2147483647 |
+| extended.cpp:8:3:8:9 | nonzero | -2147483648 | 2147483647 |
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.ql b/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.ql
index d6344e5d0629..b60e07f9f6af 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.ql
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/extended/extended.ql
@@ -1,7 +1,7 @@
 import experimental.semmle.code.cpp.rangeanalysis.ExtendedRangeAnalysis
 
-from VariableAccess expr, float lower, float upper
+from VariableAccess expr, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper
 where
   lower = lowerBound(expr) and
   upper = upperBound(expr)
-select expr, lower, upper
+select expr, lower.toString(), upper.toString()
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.expected
index e9133e191044..6b481dbecb77 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.expected
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.expected
@@ -1,9 +1,9 @@
-| extensibility.c:5:7:5:7 | x | -2.147483648E9 | 2.147483647E9 |
-| extensibility.c:5:19:5:19 | x | -10.0 | 2.147483647E9 |
-| extensibility.c:6:38:6:38 | x | -10.0 | 10.0 |
-| extensibility.c:7:12:7:17 | result | 90.0 | 110.0 |
-| extensibility.c:12:16:12:16 | x | -2.147483648E9 | 2.147483647E9 |
-| extensibility.c:12:35:12:35 | x | -2.147483648E9 | 2.147483647E9 |
-| extensibility.c:13:10:13:15 | result | 0.0 | 0.0 |
-| extensibility.c:17:3:17:23 | magic_name_at_most_10 | -2.147483648E9 | 10.0 |
-| extensibility.c:18:3:18:23 | magic_name_at_most_20 | -2.147483648E9 | 20.0 |
+| extensibility.c:5:7:5:7 | x | -2147483648 | 2147483647 |
+| extensibility.c:5:19:5:19 | x | -10 | 2147483647 |
+| extensibility.c:6:38:6:38 | x | -10 | 10 |
+| extensibility.c:7:12:7:17 | result | 90 | 110 |
+| extensibility.c:12:16:12:16 | x | -2147483648 | 2147483647 |
+| extensibility.c:12:35:12:35 | x | -2147483648 | 2147483647 |
+| extensibility.c:13:10:13:15 | result | 0 | 0 |
+| extensibility.c:17:3:17:23 | magic_name_at_most_10 | -2147483648 | 10 |
+| extensibility.c:18:3:18:23 | magic_name_at_most_20 | -2147483648 | 20 |
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.ql b/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.ql
index 0d110e67fa1e..92ccbfd5e878 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.ql
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/extensibility/extensibility.ql
@@ -6,8 +6,8 @@ import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisDefinit
 class CustomAddFunctionCall extends SimpleRangeAnalysisExpr, FunctionCall {
   CustomAddFunctionCall() { this.getTarget().hasGlobalName("custom_add_function") }
 
-  override float getLowerBounds() {
-    exists(float lower0, float lower1 |
+  override QlBuiltins::BigInt getLowerBounds() {
+    exists(QlBuiltins::BigInt lower0, QlBuiltins::BigInt lower1 |
       lower0 = getFullyConvertedLowerBounds(this.getArgument(0)) and
       lower1 = getFullyConvertedLowerBounds(this.getArgument(1)) and
       // Note: this rounds toward 0, not -Inf as it should
@@ -15,8 +15,8 @@ class CustomAddFunctionCall extends SimpleRangeAnalysisExpr, FunctionCall {
     )
   }
 
-  override float getUpperBounds() {
-    exists(float upper0, float upper1 |
+  override QlBuiltins::BigInt getUpperBounds() {
+    exists(QlBuiltins::BigInt upper0, QlBuiltins::BigInt upper1 |
       upper0 = getFullyConvertedUpperBounds(this.getArgument(0)) and
       upper1 = getFullyConvertedUpperBounds(this.getArgument(1)) and
       // Note: this rounds toward 0, not Inf as it should
@@ -33,9 +33,9 @@ class SelfSub extends SimpleRangeAnalysisExpr, SubExpr {
       this.getRightOperand().(VariableAccess).getTarget()
   }
 
-  override float getLowerBounds() { result = 0 }
+  override QlBuiltins::BigInt getLowerBounds() { result = 0.toBigInt() }
 
-  override float getUpperBounds() { result = 0 }
+  override QlBuiltins::BigInt getUpperBounds() { result = 0.toBigInt() }
 
   override predicate dependsOnChild(Expr child) { child = this.getAnOperand() }
 }
@@ -49,11 +49,11 @@ class SelfSub extends SimpleRangeAnalysisExpr, SubExpr {
  */
 class MagicParameterName extends SimpleRangeAnalysisDefinition {
   Parameter p;
-  float value;
+  QlBuiltins::BigInt value;
 
   MagicParameterName() {
     this.definedByParameter(p) and
-    value = p.getName().regexpCapture("magic_name_at_most_(\\d+)", 1).toFloat()
+    value = p.getName().regexpCapture("magic_name_at_most_(\\d+)", 1).toBigInt()
   }
 
   override predicate hasRangeInformationFor(StackVariable v) { v = p }
@@ -63,19 +63,19 @@ class MagicParameterName extends SimpleRangeAnalysisDefinition {
     none()
   }
 
-  override float getLowerBounds(StackVariable var) {
+  override QlBuiltins::BigInt getLowerBounds(StackVariable var) {
     var = p and
     result = typeLowerBound(p.getUnspecifiedType())
   }
 
-  override float getUpperBounds(StackVariable var) {
+  override QlBuiltins::BigInt getUpperBounds(StackVariable var) {
     var = p and
     result = value
   }
 }
 
-from VariableAccess expr, float lower, float upper
+from VariableAccess expr, QlBuiltins::BigInt lower, QlBuiltins::BigInt upper
 where
   lower = lowerBound(expr) and
   upper = upperBound(expr)
-select expr, lower, upper
+select expr, lower.toString(), upper.toString()
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.expected b/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.expected
index f714ac312ea7..6fe0ec239b62 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.expected
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.expected
@@ -1,2 +1,2 @@
-| test.cpp:4:3:4:8 | call to strlen | 7.0 | 7.0 |
-| test.cpp:5:3:5:8 | call to strlen | 1.8446744073709552E19 | 0.0 |
+| test.cpp:4:3:4:8 | call to strlen | 7 | 7 |
+| test.cpp:5:3:5:8 | call to strlen | 18446744073709551615 | 0 |
diff --git a/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.ql b/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.ql
index c77b20786109..59016bf0d48b 100644
--- a/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.ql
+++ b/cpp/ql/test/experimental/library-tests/rangeanalysis/strlenliteral/StrlenLiteralRange.ql
@@ -3,4 +3,4 @@ import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 import experimental.semmle.code.cpp.rangeanalysis.extensions.StrlenLiteralRangeExpr
 
 from FunctionCall fc
-select fc, upperBound(fc), lowerBound(fc)
+select fc, upperBound(fc).toString(), lowerBound(fc).toString()
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected
index 112b6cb02014..482073673d8a 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected
@@ -486,13 +486,13 @@
 | test.c:470:3:470:4 | xy | 0 |
 | test.c:470:8:470:8 | x | 1000000003 |
 | test.c:470:12:470:12 | y | 1000000003 |
-| test.c:471:10:471:11 | xy | 1000000006000000000 |
+| test.c:471:10:471:11 | xy | 1000000006000000009 |
 | test.c:476:3:476:3 | x | 0 |
 | test.c:477:3:477:3 | y | 0 |
 | test.c:478:3:478:4 | xy | 0 |
 | test.c:478:8:478:8 | x | 274177 |
 | test.c:478:12:478:12 | y | 67280421310721 |
-| test.c:479:10:479:11 | xy | 18446744073709551616 |
+| test.c:479:10:479:11 | xy | 0 |
 | test.c:483:7:483:8 | ui | 0 |
 | test.c:484:43:484:44 | ui | 10 |
 | test.c:484:48:484:49 | ui | 10 |
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected
index f012490f1156..d46d390c0497 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected
@@ -1,19 +1,19 @@
-| test.c:154:10:154:40 | ... ? ... : ... | -1.0 | 1.0 | -1.0 |
-| test.c:357:8:357:23 | ... ? ... : ... | 0.0 | 0.0 | 10.0 |
-| test.c:358:8:358:24 | ... ? ... : ... | 0.0 | 10.0 | 0.0 |
-| test.c:366:10:366:15 | ... ? ... : ... | 0.0 | 0.0 | 5.0 |
-| test.c:367:10:367:17 | ... ? ... : ... | 0.0 | 0.0 | 500.0 |
-| test.c:368:10:368:21 | ... ? ... : ... | 1.0 | 1.0 | 500.0 |
-| test.c:369:10:369:36 | ... ? ... : ... | 0.0 | 1.0 | 5.0 |
-| test.c:370:10:370:38 | ... ? ... : ... | 0.0 | 1.0 | 500.0 |
-| test.c:371:10:371:39 | ... ? ... : ... | 1.0 | 1.0 | 500.0 |
-| test.c:379:8:379:24 | ... ? ... : ... | 101.0 | 101.0 | 110.0 |
-| test.c:380:8:380:25 | ... ? ... : ... | 101.0 | 110.0 | 101.0 |
-| test.c:385:10:385:21 | ... ? ... : ... | 0.0 | 0.0 | 5.0 |
-| test.c:386:10:386:21 | ... ? ... : ... | 100.0 | 100.0 | 5.0 |
-| test.c:387:10:387:38 | ... ? ... : ... | 0.0 | 100.0 | 5.0 |
-| test.c:394:20:394:36 | ... ? ... : ... | 0.0 | 0.0 | 100.0 |
-| test.c:606:5:606:14 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
-| test.c:607:5:607:14 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |
-| test.cpp:121:3:121:12 | ... ? ... : ... | 0.0 | 1.0 | 0.0 |
-| test.cpp:122:3:122:12 | ... ? ... : ... | 0.0 | 0.0 | 1.0 |
+| test.c:154:10:154:40 | ... ? ... : ... | -1 | 1 | -1 |
+| test.c:357:8:357:23 | ... ? ... : ... | 0 | 0 | 10 |
+| test.c:358:8:358:24 | ... ? ... : ... | 0 | 10 | 0 |
+| test.c:366:10:366:15 | ... ? ... : ... | 0 | 0 | 5 |
+| test.c:367:10:367:17 | ... ? ... : ... | 0 | 0 | 500 |
+| test.c:368:10:368:21 | ... ? ... : ... | 1 | 1 | 500 |
+| test.c:369:10:369:36 | ... ? ... : ... | 0 | 1 | 5 |
+| test.c:370:10:370:38 | ... ? ... : ... | 0 | 1 | 500 |
+| test.c:371:10:371:39 | ... ? ... : ... | 1 | 1 | 500 |
+| test.c:379:8:379:24 | ... ? ... : ... | 101 | 101 | 110 |
+| test.c:380:8:380:25 | ... ? ... : ... | 101 | 110 | 101 |
+| test.c:385:10:385:21 | ... ? ... : ... | 0 | 0 | 5 |
+| test.c:386:10:386:21 | ... ? ... : ... | 100 | 100 | 5 |
+| test.c:387:10:387:38 | ... ? ... : ... | 0 | 100 | 5 |
+| test.c:394:20:394:36 | ... ? ... : ... | 0 | 0 | 100 |
+| test.c:606:5:606:14 | ... ? ... : ... | 0 | 1 | 0 |
+| test.c:607:5:607:14 | ... ? ... : ... | 0 | 0 | 1 |
+| test.cpp:121:3:121:12 | ... ? ... : ... | 0 | 1 | 0 |
+| test.cpp:122:3:122:12 | ... ? ... : ... | 0 | 0 | 1 |
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.ql b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.ql
index f4065881bcc9..d1a7839a84f6 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.ql
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.ql
@@ -2,4 +2,5 @@ import cpp
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 
 from ConditionalExpr ce
-select ce, lowerBound(ce), lowerBound(ce.getThen()), lowerBound(ce.getElse())
+select ce, lowerBound(ce).toString(), lowerBound(ce.getThen()).toString(),
+  lowerBound(ce.getElse()).toString()
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected
index 8a387c3ae464..527a4d4381d3 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected
@@ -1,19 +1,19 @@
-| test.c:154:10:154:40 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | -1.0 |
-| test.c:357:8:357:23 | ... ? ... : ... | 99.0 | 99.0 | 10.0 |
-| test.c:358:8:358:24 | ... ? ... : ... | 99.0 | 10.0 | 99.0 |
-| test.c:366:10:366:15 | ... ? ... : ... | 299.0 | 299.0 | 5.0 |
-| test.c:367:10:367:17 | ... ? ... : ... | 500.0 | 299.0 | 500.0 |
-| test.c:368:10:368:21 | ... ? ... : ... | 300.0 | 300.0 | 500.0 |
-| test.c:369:10:369:36 | ... ? ... : ... | 255.0 | 300.0 | 5.0 |
-| test.c:370:10:370:38 | ... ? ... : ... | 500.0 | 300.0 | 500.0 |
-| test.c:371:10:371:39 | ... ? ... : ... | 300.0 | 300.0 | 500.0 |
-| test.c:379:8:379:24 | ... ? ... : ... | 4.294967295E9 | 4.294967295E9 | 110.0 |
-| test.c:380:8:380:25 | ... ? ... : ... | 4.294967295E9 | 110.0 | 4.294967295E9 |
-| test.c:385:10:385:21 | ... ? ... : ... | 4.294967295E9 | 4.294967295E9 | 5.0 |
-| test.c:386:10:386:21 | ... ? ... : ... | 4.294967295E9 | 4.294967295E9 | 5.0 |
-| test.c:387:10:387:38 | ... ? ... : ... | 255.0 | 4.294967295E9 | 5.0 |
-| test.c:394:20:394:36 | ... ? ... : ... | 100.0 | 99.0 | 100.0 |
-| test.c:606:5:606:14 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
-| test.c:607:5:607:14 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |
-| test.cpp:121:3:121:12 | ... ? ... : ... | 32767.0 | 32767.0 | 0.0 |
-| test.cpp:122:3:122:12 | ... ? ... : ... | 32767.0 | 0.0 | 32767.0 |
+| test.c:154:10:154:40 | ... ? ... : ... | 2147483647 | 2147483647 | -1 |
+| test.c:357:8:357:23 | ... ? ... : ... | 99 | 99 | 10 |
+| test.c:358:8:358:24 | ... ? ... : ... | 99 | 10 | 99 |
+| test.c:366:10:366:15 | ... ? ... : ... | 299 | 299 | 5 |
+| test.c:367:10:367:17 | ... ? ... : ... | 500 | 299 | 500 |
+| test.c:368:10:368:21 | ... ? ... : ... | 300 | 300 | 500 |
+| test.c:369:10:369:36 | ... ? ... : ... | 255 | 300 | 5 |
+| test.c:370:10:370:38 | ... ? ... : ... | 500 | 300 | 500 |
+| test.c:371:10:371:39 | ... ? ... : ... | 300 | 300 | 500 |
+| test.c:379:8:379:24 | ... ? ... : ... | 4294967295 | 4294967295 | 110 |
+| test.c:380:8:380:25 | ... ? ... : ... | 4294967295 | 110 | 4294967295 |
+| test.c:385:10:385:21 | ... ? ... : ... | 4294967295 | 4294967295 | 5 |
+| test.c:386:10:386:21 | ... ? ... : ... | 4294967295 | 4294967295 | 5 |
+| test.c:387:10:387:38 | ... ? ... : ... | 255 | 4294967295 | 5 |
+| test.c:394:20:394:36 | ... ? ... : ... | 100 | 99 | 100 |
+| test.c:606:5:606:14 | ... ? ... : ... | 32767 | 32767 | 0 |
+| test.c:607:5:607:14 | ... ? ... : ... | 32767 | 0 | 32767 |
+| test.cpp:121:3:121:12 | ... ? ... : ... | 32767 | 32767 | 0 |
+| test.cpp:122:3:122:12 | ... ? ... : ... | 32767 | 0 | 32767 |
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.ql b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.ql
index 409735829361..b4736fd5a683 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.ql
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.ql
@@ -2,4 +2,5 @@ import cpp
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 
 from ConditionalExpr ce
-select ce, upperBound(ce), upperBound(ce.getThen()), upperBound(ce.getElse())
+select ce, upperBound(ce).toString(), upperBound(ce.getThen()).toString(),
+  upperBound(ce.getElse()).toString()
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c
index 8c7978ac4aa6..571cda50a7c3 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c
@@ -468,7 +468,7 @@ unsigned long mult_rounding() {
   unsigned long x, y, xy;
   x = y = 1000000003UL; // 1e9 + 3
   xy = x * y;
-  return xy; // BUG: upper bound should be >= 1000000006000000009UL
+  return xy; // = 1000000006000000009UL
 }
 
 unsigned long mult_overflow() {
@@ -482,7 +482,7 @@ unsigned long mult_overflow() {
 unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
   if (ui >= 10) {
     unsigned long result = (unsigned long)ui * ui;
-    return result; // BUG: upper bound should be >= 18446744065119617025
+    return result; // = 18446744065119617025UL
   }
   if (ul >= 10) {
     unsigned long result = ul * ul;
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected
index 8772a763a4d3..659081cf26a8 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected
@@ -73,10 +73,10 @@
 | test.c:105:5:105:5 | c | 127 |
 | test.c:106:9:106:9 | c | 127 |
 | test.c:109:9:109:9 | c | 127 |
-| test.c:119:10:119:10 | n | 18446744073709551616 |
-| test.c:124:11:124:15 | Start | 18446744073709551616 |
-| test.c:127:6:127:10 | Start | 18446744073709551616 |
-| test.c:127:15:127:20 | Length | 18446744073709551616 |
+| test.c:119:10:119:10 | n | 18446744073709551615 |
+| test.c:124:11:124:15 | Start | 18446744073709551615 |
+| test.c:127:6:127:10 | Start | 18446744073709551615 |
+| test.c:127:15:127:20 | Length | 18446744073709551615 |
 | test.c:135:22:135:22 | c | 127 |
 | test.c:137:20:137:20 | x | 0 |
 | test.c:138:11:138:11 | i | 2147483647 |
@@ -98,9 +98,9 @@
 | test.c:150:25:150:26 | x3 | 2147483647 |
 | test.c:150:30:150:31 | c0 | 127 |
 | test.c:150:35:150:36 | s0 | 65535 |
-| test.c:154:11:154:11 | x | 9223372036854775808 |
-| test.c:154:20:154:20 | x | 9223372036854775808 |
-| test.c:154:30:154:30 | x | 9223372036854775808 |
+| test.c:154:11:154:11 | x | 9223372036854775807 |
+| test.c:154:20:154:20 | x | 9223372036854775807 |
+| test.c:154:30:154:30 | x | 9223372036854775807 |
 | test.c:154:35:154:35 | x | 2147483647 |
 | test.c:161:12:161:12 | a | 2147483647 |
 | test.c:161:17:161:17 | a | 2147483647 |
@@ -481,26 +481,26 @@
 | test.c:461:5:461:9 | total | 506 |
 | test.c:461:14:461:14 | r | 253 |
 | test.c:464:10:464:14 | total | 759 |
-| test.c:469:3:469:3 | x | 18446744073709551616 |
-| test.c:469:7:469:7 | y | 18446744073709551616 |
-| test.c:470:3:470:4 | xy | 18446744073709551616 |
+| test.c:469:3:469:3 | x | 18446744073709551615 |
+| test.c:469:7:469:7 | y | 18446744073709551615 |
+| test.c:470:3:470:4 | xy | 18446744073709551615 |
 | test.c:470:8:470:8 | x | 1000000003 |
 | test.c:470:12:470:12 | y | 1000000003 |
-| test.c:471:10:471:11 | xy | 1000000006000000000 |
-| test.c:476:3:476:3 | x | 18446744073709551616 |
-| test.c:477:3:477:3 | y | 18446744073709551616 |
-| test.c:478:3:478:4 | xy | 18446744073709551616 |
+| test.c:471:10:471:11 | xy | 1000000006000000009 |
+| test.c:476:3:476:3 | x | 18446744073709551615 |
+| test.c:477:3:477:3 | y | 18446744073709551615 |
+| test.c:478:3:478:4 | xy | 18446744073709551615 |
 | test.c:478:8:478:8 | x | 274177 |
 | test.c:478:12:478:12 | y | 67280421310721 |
-| test.c:479:10:479:11 | xy | 18446744073709551616 |
+| test.c:479:10:479:11 | xy | 18446744073709551615 |
 | test.c:483:7:483:8 | ui | 4294967295 |
 | test.c:484:43:484:44 | ui | 4294967295 |
 | test.c:484:48:484:49 | ui | 4294967295 |
-| test.c:485:12:485:17 | result | 18446744065119617024 |
-| test.c:487:7:487:8 | ul | 18446744073709551616 |
-| test.c:488:28:488:29 | ul | 18446744073709551616 |
-| test.c:488:33:488:34 | ul | 18446744073709551616 |
-| test.c:489:12:489:17 | result | 18446744073709551616 |
+| test.c:485:12:485:17 | result | 18446744065119617025 |
+| test.c:487:7:487:8 | ul | 18446744073709551615 |
+| test.c:488:28:488:29 | ul | 18446744073709551615 |
+| test.c:488:33:488:34 | ul | 18446744073709551615 |
+| test.c:489:12:489:17 | result | 18446744073709551615 |
 | test.c:495:7:495:8 | ui | 4294967295 |
 | test.c:495:19:495:20 | ui | 10 |
 | test.c:496:5:496:6 | ui | 10 |
diff --git a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c
index fd1bc655051d..6e4c063b8cfb 100644
--- a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c	
+++ b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c	
@@ -401,8 +401,8 @@ void mult_rounding() {
   // are no PointlessComparison false positives in these tests because alerts
   // are suppressed when ulp() < 1, which roughly means that the number is
   // larger than 2^53.
-  if (x * y < xy) {} // always false [NOT DETECTED]
-  if (x * y > xy) {} // always false [NOT DETECTED]
+  if (x * y < xy) {} // always false
+  if (x * y > xy) {} // always false
 }
 
 void mult_overflow() {
@@ -411,7 +411,7 @@ void mult_overflow() {
   // to 64-bit unsigned.
   x = 274177UL;
   y = 67280421310721UL;
-  if (x * y == 1) {} // always true [BUG: reported as always false]
+  if (x * y == 1) {} // always true [NOT DETECTED]
 
   // This bug appears to be caused by
   // `RangeAnalysisUtils::typeUpperBound(unsigned long)` having a result of
diff --git a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.cpp b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.cpp
index 7b67f77ad443..b9824a27ece8 100644
--- a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.cpp	
+++ b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.cpp	
@@ -6,7 +6,7 @@ struct A {
     const int int_member = 0;
     A(int n) : int_member(n) {
         if(int_member <= 10) {
-                    
+
         }
     }
 };
@@ -34,12 +34,12 @@ int extreme_values(void)
 	unsigned long long int y = 0xFFFFFFFFFFFF;
 
 	if (x >> 1 >= 0xFFFFFFFFFFFFFFFF) {} // always false
-	if (x >> 1 >= 0x8000000000000000) {} // always false [NOT DETECTED]
-	if (x >> 1 >= 0x7FFFFFFFFFFFFFFF) {} // always true [NOT DETECTED]
-	if (x >> 1 >= 0xFFFFFFFFFFFFFFF) {} // always true [NOT DETECTED]
-
-	if (y >> 1 >= 0xFFFFFFFFFFFF) {} // always false [INCORRECT MESSAGE]
-	if (y >> 1 >= 0x800000000000) {} // always false [INCORRECT MESSAGE]
-	if (y >> 1 >= 0x7FFFFFFFFFFF) {} // always true [INCORRECT MESSAGE]
-	if (y >> 1 >= 0xFFFFFFFFFFF) {} // always true [INCORRECT MESSAGE]
+	if (x >> 1 >= 0x8000000000000000) {} // always false
+	if (x >> 1 >= 0x7FFFFFFFFFFFFFFF) {} // always true
+	if (x >> 1 >= 0xFFFFFFFFFFFFFFF) {} // always true
+
+	if (y >> 1 >= 0xFFFFFFFFFFFF) {} // always false
+	if (y >> 1 >= 0x800000000000) {} // always false
+	if (y >> 1 >= 0x7FFFFFFFFFFF) {} // always true
+	if (y >> 1 >= 0xFFFFFFFFFFF) {} // always true
 }
diff --git a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.expected b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.expected
index 6c273b985eeb..29c5929dfb73 100644
--- a/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.expected	
+++ b/cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.expected	
@@ -43,11 +43,15 @@
 | PointlessComparison.c:383:6:383:17 | ... >= ... | Comparison is always false because ... & ... <= 2. |
 | PointlessComparison.c:388:10:388:21 | ... > ... | Comparison is always false because ... * ... <= 408. |
 | PointlessComparison.c:391:12:391:20 | ... < ... | Comparison is always false because ... * ... >= 6. |
-| PointlessComparison.c:414:7:414:16 | ... == ... | Comparison is always false because ... * ... >= 18446744073709551616. |
-| PointlessComparison.cpp:36:6:36:33 | ... >= ... | Comparison is always false because ... >> ... <= 9223372036854775808. |
-| PointlessComparison.cpp:41:6:41:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327.5. |
-| PointlessComparison.cpp:42:6:42:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327.5. |
-| PointlessComparison.cpp:43:6:43:29 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327.5. |
-| PointlessComparison.cpp:44:6:44:28 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327.5. |
+| PointlessComparison.c:404:7:404:16 | ... < ... | Comparison is always false because ... * ... >= 1000000006000000009 and 1000000006000000009 >= xy. |
+| PointlessComparison.c:405:7:405:16 | ... > ... | Comparison is always false because ... * ... <= 1000000006000000009 and 1000000006000000009 <= xy. |
+| PointlessComparison.cpp:36:6:36:33 | ... >= ... | Comparison is always false because ... >> ... <= 9223372036854775807. |
+| PointlessComparison.cpp:37:6:37:33 | ... >= ... | Comparison is always false because ... >> ... <= 9223372036854775807. |
+| PointlessComparison.cpp:38:6:38:33 | ... >= ... | Comparison is always true because ... >> ... >= 9223372036854775807. |
+| PointlessComparison.cpp:39:6:39:32 | ... >= ... | Comparison is always true because ... >> ... >= 9223372036854775807. |
+| PointlessComparison.cpp:41:6:41:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327. |
+| PointlessComparison.cpp:42:6:42:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327. |
+| PointlessComparison.cpp:43:6:43:29 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327. |
+| PointlessComparison.cpp:44:6:44:28 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327. |
 | RegressionTests.cpp:57:7:57:22 | ... <= ... | Comparison is always true because * ... <= 4294967295. |
 | Templates.cpp:9:10:9:24 | ... <= ... | Comparison is always true because local <= 32767. |

From 5fa02d6ebac8c0225c5db895c7fd5e58184100ef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Fri, 29 Nov 2024 12:10:05 +0100
Subject: [PATCH 4/6] Un-inline parseAsBigInt

---
 .../cpp/rangeanalysis/RangeAnalysisUtils.qll  | 24 ++++++++++---------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
index 0b11a25bc3d9..acea31874013 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
@@ -484,18 +484,20 @@ QlBuiltins::BigInt varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecif
  */
 QlBuiltins::BigInt infinityAsBigInt() { result = 1.toBigInt().bitShiftLeft(1024) }
 
-bindingset[s]
 QlBuiltins::BigInt parseAsBigInt(string s) {
-  result = s.toBigInt()
-  or
-  s.toFloat() = 1.0 / 0.0 and result = infinityAsBigInt()
-  or
-  s.toFloat() = -(1.0 / 0.0) and result = -infinityAsBigInt()
-  or
-  exists(QlBuiltins::BigInt coeff, int base10exp | parseFiniteAsBigInt(s, coeff, base10exp) |
-    if base10exp < 0
-    then result = coeff / 10.toBigInt().pow(-base10exp)
-    else result = coeff * 10.toBigInt().pow(base10exp)
+  s = any(Expr e).getValue() and
+  (
+    result = s.toBigInt()
+    or
+    s.toFloat() = 1.0 / 0.0 and result = infinityAsBigInt()
+    or
+    s.toFloat() = -(1.0 / 0.0) and result = -infinityAsBigInt()
+    or
+    exists(QlBuiltins::BigInt coeff, int base10exp | parseFiniteAsBigInt(s, coeff, base10exp) |
+      if base10exp < 0
+      then result = coeff / 10.toBigInt().pow(-base10exp)
+      else result = coeff * 10.toBigInt().pow(base10exp)
+    )
   )
 }
 

From 544fcdd0c392cf06212e6d14f49402095d44dd98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Fri, 29 Nov 2024 13:20:38 +0100
Subject: [PATCH 5/6] Simplify parseAsBigInt even further

---
 .../cpp/rangeanalysis/RangeAnalysisUtils.qll  | 67 +++----------------
 .../SimpleRangeAnalysis/upperBound.ql         | 12 +++-
 2 files changed, 21 insertions(+), 58 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
index acea31874013..b852dc3957a1 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
@@ -485,61 +485,16 @@ QlBuiltins::BigInt varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecif
 QlBuiltins::BigInt infinityAsBigInt() { result = 1.toBigInt().bitShiftLeft(1024) }
 
 QlBuiltins::BigInt parseAsBigInt(string s) {
-  s = any(Expr e).getValue() and
-  (
-    result = s.toBigInt()
-    or
-    s.toFloat() = 1.0 / 0.0 and result = infinityAsBigInt()
-    or
-    s.toFloat() = -(1.0 / 0.0) and result = -infinityAsBigInt()
-    or
-    exists(QlBuiltins::BigInt coeff, int base10exp | parseFiniteAsBigInt(s, coeff, base10exp) |
-      if base10exp < 0
-      then result = coeff / 10.toBigInt().pow(-base10exp)
-      else result = coeff * 10.toBigInt().pow(base10exp)
-    )
-  )
-}
-
-bindingset[s]
-private predicate parseFiniteAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
-  exists(string t | s = "+" + t | parseUnsignedAsBigInt(t, coeff, base10exp))
-  or
-  exists(string t | s = "-" + t | parseUnsignedAsBigInt(t, -coeff, base10exp))
-  or
-  parseUnsignedAsBigInt(s, coeff, base10exp)
-}
-
-bindingset[s]
-private predicate parseUnsignedAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
-  exists(string beforeE, int base10expAfterE, int base10expBeforeE |
-    beforeE = s.toUpperCase().splitAt("E", 0) and
-    base10expAfterE = parseSignedInt(s.toUpperCase().splitAt("E", 1)) and
-    parseUnsignedDecimalAsBigInt(beforeE, coeff, base10expBeforeE) and
-    base10exp = base10expBeforeE + base10expAfterE
-  )
-  or
-  exists(string beforeDot, string afterDot |
-    beforeDot = s.splitAt(".", 0) and
-    afterDot = s.splitAt(".", 1) and
-    coeff = (beforeDot + afterDot).toBigInt() and
-    base10exp = -afterDot.length()
-  )
-}
-
-bindingset[s]
-private predicate parseUnsignedDecimalAsBigInt(string s, QlBuiltins::BigInt coeff, int base10exp) {
-  exists(string beforeDot, string afterDot |
-    beforeDot = s.splitAt(".", 0) and
-    afterDot = s.splitAt(".", 1) and
-    coeff = (beforeDot + afterDot).toBigInt() and
-    base10exp = -afterDot.length()
+  exists(Expr e | s = e.getValue() |
+    if exists(s.toBigInt()) then
+      result = s.toBigInt()
+    else
+      exists(float f | f = s.toFloat() |
+        f = 1.0 / 0.0 and result = infinityAsBigInt()
+        or
+        f = -(1.0 / 0.0) and result = -infinityAsBigInt()
+        or
+        result = f.toString().toBigInt()
+      )
   )
 }
-
-bindingset[s]
-private int parseSignedInt(string s) {
-  exists(string t | s = "+" + t | result = t.toInt())
-  or
-  result = s.toInt()
-}
diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.ql b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.ql
index 26d188ce89cb..399891d308c2 100644
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.ql
+++ b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.ql
@@ -1,4 +1,12 @@
 import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
+import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
-from VariableAccess expr
-select expr, upperBound(expr).toString()
+from VariableAccess expr, QlBuiltins::BigInt u, string s
+where
+  u = upperBound(expr) and
+  if u = infinityAsBigInt()
+  then s = "Infinity"
+  else if u = -infinityAsBigInt()
+  then s = "-Infinity"
+  else s = u.toString()
+select expr, s

From 3a233cc828ca2692f2c16aea7fc14c2c3fbdd286 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nora=20Dimitrijevi=C4=87?= <d10c@users.noreply.github.com>
Date: Fri, 29 Nov 2024 13:55:24 +0100
Subject: [PATCH 6/6] Reinstate bindingset[s] on parseAsBigInt

---
 .../cpp/rangeanalysis/RangeAnalysisUtils.qll  | 23 +++++++++----------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
index b852dc3957a1..45351fff3e82 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/RangeAnalysisUtils.qll
@@ -484,17 +484,16 @@ QlBuiltins::BigInt varMaxVal(Variable v) { result = typeUpperBound(v.getUnspecif
  */
 QlBuiltins::BigInt infinityAsBigInt() { result = 1.toBigInt().bitShiftLeft(1024) }
 
+bindingset[s]
 QlBuiltins::BigInt parseAsBigInt(string s) {
-  exists(Expr e | s = e.getValue() |
-    if exists(s.toBigInt()) then
-      result = s.toBigInt()
-    else
-      exists(float f | f = s.toFloat() |
-        f = 1.0 / 0.0 and result = infinityAsBigInt()
-        or
-        f = -(1.0 / 0.0) and result = -infinityAsBigInt()
-        or
-        result = f.toString().toBigInt()
-      )
-  )
+  if exists(s.toBigInt()) then
+    result = s.toBigInt()
+  else
+    exists(float f | f = s.toFloat() |
+      f = 1.0 / 0.0 and result = infinityAsBigInt()
+      or
+      f = -(1.0 / 0.0) and result = -infinityAsBigInt()
+      or
+      result = f.toString().toBigInt()
+    )
 }