diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql
new file mode 100644
index 000000000..3d54b4f82
--- /dev/null
+++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql
@@ -0,0 +1,147 @@
+/**
+ * @id c/misra/possible-misuse-of-undetected-infinity
+ * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of infinities
+ * @description Evaluation of floating-point expressions shall not lead to the undetected generation
+ *              of infinities.
+ * @kind path-problem
+ * @precision medium
+ * @problem.severity warning
+ * @tags external/misra/id/dir-4-15
+ *       correctness
+ *       external/misra/c/2012/amendment3
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codeql.util.Boolean
+import codingstandards.c.misra
+import codingstandards.cpp.RestrictedRangeAnalysis
+import codingstandards.cpp.FloatingPoint
+import codingstandards.cpp.AlertReporting
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.dataflow.new.DataFlow
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.controlflow.Dominance
+
+module InvalidInfinityUsage implements DataFlow::ConfigSig {
+  /**
+   * An operation which does not have Infinity as an input, but may produce Infinity, according
+   * to the `RestrictedRangeAnalysis` module.
+   */
+  predicate isSource(DataFlow::Node node) {
+    potentialSource(node) and
+    not exists(DataFlow::Node prior |
+      isAdditionalFlowStep(prior, node) and
+      potentialSource(prior)
+    )
+  }
+
+  /**
+   * An operation which may produce Infinity acconding to the `RestrictedRangeAnalysis` module.
+   */
+  additional predicate potentialSource(DataFlow::Node node) {
+    node.asExpr() instanceof Operation and
+    exprMayEqualInfinity(node.asExpr(), _)
+  }
+
+  predicate isBarrierOut(DataFlow::Node node) {
+    guardedNotFPClass(node.asExpr(), TInfinite())
+    or
+    exists(Expr e |
+      e.getType() instanceof IntegralType and
+      e = node.asConvertedExpr()
+    )
+  }
+
+  /**
+   * An additional flow step to handle operations which propagate Infinity.
+   *
+   * This double checks that an Infinity may propagate by checking the `RestrictedRangeAnalysis`
+   * value estimate. This is conservative, since `RestrictedRangeAnalysis` is performed locally
+   * in scope with unanalyzable values in a finite range. However, this conservative approach
+   * leverages analysis of guards and other local conditions to avoid false positives.
+   */
+  predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
+    exists(Operation o |
+      o.getAnOperand() = source.asExpr() and
+      o = sink.asExpr() and
+      potentialSource(sink)
+    )
+  }
+
+  predicate isSink(DataFlow::Node node) {
+    node instanceof InvalidInfinityUsage and
+    (
+      // Require that range analysis finds this value potentially infinite, to avoid false positives
+      // in the presence of guards. This may induce false negatives.
+      exprMayEqualInfinity(node.asExpr(), _)
+      or
+      // Unanalyzable expressions are not checked against range analysis, which assumes a finite
+      // range.
+      not RestrictedRangeAnalysis::canBoundExpr(node.asExpr())
+      or
+      node.asExpr().(VariableAccess).getTarget() instanceof Parameter
+    )
+  }
+}
+
+class InvalidInfinityUsage extends DataFlow::Node {
+  string description;
+  string infinityDescription;
+
+  InvalidInfinityUsage() {
+    // Case 2: NaNs and infinities shall not be cast to integers
+    exists(Conversion c |
+      asExpr() = c.getUnconverted() and
+      c.getExpr().getType() instanceof FloatingPointType and
+      c.getType() instanceof IntegralType and
+      description = "$@ casted to integer." and
+      infinityDescription = "Possibly infinite float value"
+    )
+    or
+    // Case 3: Infinities shall not underflow or otherwise produce finite values
+    exists(BinaryOperation op |
+      asExpr() = op.getRightOperand() and
+      op.getOperator() = "/" and
+      description = "Division operation may silently underflow and produce zero, as the divisor $@." and
+      infinityDescription = "may be an infinite float value"
+    )
+  }
+
+  string getDescription() { result = description }
+
+  string getInfinityDescription() { result = infinityDescription }
+}
+
+module InvalidInfinityFlow = DataFlow::Global<InvalidInfinityUsage>;
+
+import InvalidInfinityFlow::PathGraph
+
+from
+  Element elem, InvalidInfinityFlow::PathNode source, InvalidInfinityFlow::PathNode sink,
+  InvalidInfinityUsage usage, Expr sourceExpr, Element extra, string extraString
+where
+  elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
+  not InvalidInfinityFlow::PathGraph::edges(_, source, _, _) and
+  not InvalidInfinityFlow::PathGraph::edges(sink, _, _, _) and
+  not isExcluded(elem, FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery()) and
+  not sourceExpr.isFromTemplateInstantiation(_) and
+  not usage.asExpr().isFromTemplateInstantiation(_) and
+  usage = sink.getNode() and
+  sourceExpr = source.getNode().asExpr() and
+  InvalidInfinityFlow::flow(source.getNode(), usage) and
+  (
+    if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
+    then
+      extraString =
+        usage.getInfinityDescription() + " computed in function " +
+          sourceExpr.getEnclosingFunction().getName() and
+      extra = sourceExpr.getEnclosingFunction()
+    else (
+      extra = sourceExpr and
+      if sourceExpr instanceof DivExpr
+      then extraString = usage.getInfinityDescription() + " from division by zero"
+      else extraString = usage.getInfinityDescription()
+    )
+  )
+select elem, source, sink, usage.getDescription(), extra, extraString
diff --git a/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql
new file mode 100644
index 000000000..2835a454d
--- /dev/null
+++ b/c/misra/src/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql
@@ -0,0 +1,257 @@
+/**
+ * @id c/misra/possible-misuse-of-undetected-na-n
+ * @name DIR-4-15: Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs
+ * @description Evaluation of floating-point expressions shall not lead to the undetected generation
+ *              of NaNs.
+ * @kind path-problem
+ * @precision low
+ * @problem.severity warning
+ * @tags external/misra/id/dir-4-15
+ *       correctness
+ *       external/misra/c/2012/amendment3
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codeql.util.Boolean
+import codingstandards.c.misra
+import codingstandards.cpp.RestrictedRangeAnalysis
+import codingstandards.cpp.FloatingPoint
+import codingstandards.cpp.AlertReporting
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.dataflow.new.DataFlow
+import semmle.code.cpp.dataflow.new.TaintTracking
+import semmle.code.cpp.controlflow.Dominance
+
+bindingset[name]
+Function getMathVariants(string name) { result.hasGlobalOrStdName([name, name + "f", name + "l"]) }
+
+predicate hasDomainError(FunctionCall fc, string description) {
+  exists(Function functionWithDomainError | fc.getTarget() = functionWithDomainError |
+    functionWithDomainError = [getMathVariants(["acos", "asin", "atanh"])] and
+    not (
+      RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) <= 1.0 and
+      RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) >= -1.0
+    ) and
+    description =
+      "the argument has a range " + RestrictedRangeAnalysis::lowerBound(fc.getArgument(0)) + "..." +
+        RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) +
+        " which is outside the domain of this function (-1.0...1.0)"
+    or
+    functionWithDomainError = getMathVariants(["atan2", "pow"]) and
+    (
+      exprMayEqualZero(fc.getArgument(0)) and
+      exprMayEqualZero(fc.getArgument(1)) and
+      description = "both arguments are equal to zero"
+    )
+    or
+    functionWithDomainError = getMathVariants("pow") and
+    (
+      RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and
+      RestrictedRangeAnalysis::upperBound(fc.getArgument(1)) < 0.0 and
+      description = "both arguments are less than zero"
+    )
+    or
+    functionWithDomainError = getMathVariants("acosh") and
+    RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 1.0 and
+    description = "argument is less than 1"
+    or
+    //pole error is the same as domain for logb and tgamma (but not ilogb - no pole error exists)
+    functionWithDomainError = getMathVariants(["ilogb", "logb", "tgamma"]) and
+    exprMayEqualZero(fc.getArgument(0)) and
+    description = "argument is equal to zero"
+    or
+    functionWithDomainError = getMathVariants(["log", "log10", "log2", "sqrt"]) and
+    RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < 0.0 and
+    description = "argument is negative"
+    or
+    functionWithDomainError = getMathVariants("log1p") and
+    RestrictedRangeAnalysis::upperBound(fc.getArgument(0)) < -1.0 and
+    description = "argument is less than 1"
+    or
+    functionWithDomainError = getMathVariants("fmod") and
+    exprMayEqualZero(fc.getArgument(1)) and
+    description = "y is 0"
+  )
+}
+
+abstract class PotentiallyNaNExpr extends Expr {
+  abstract string getReason();
+}
+
+class DomainErrorFunctionCall extends FunctionCall, PotentiallyNaNExpr {
+  string reason;
+
+  DomainErrorFunctionCall() { hasDomainError(this, reason) }
+
+  override string getReason() { result = reason }
+}
+
+// IEEE 754-1985 Section 7.1 invalid operations
+class InvalidOperationExpr extends BinaryOperation, PotentiallyNaNExpr {
+  string reason;
+
+  InvalidOperationExpr() {
+    // Usual arithmetic conversions in both languages mean that if either operand is a floating
+    // type, the other one is converted to a floating type as well.
+    getAnOperand().getFullyConverted().getType() instanceof FloatingPointType and
+    (
+      // 7.1.1 propagates signaling NaNs, we rely on flow analysis and/or assume quiet NaNs, so we
+      // intentionally do not cover this case.
+      // 7.1.2: magnitude subtraction of infinities, such as +Inf + -Inf
+      getOperator() = "+" and
+      exists(Boolean sign |
+        exprMayEqualInfinity(getLeftOperand(), sign) and
+        exprMayEqualInfinity(getRightOperand(), sign.booleanNot())
+      ) and
+      reason = "from addition of infinity and negative infinity"
+      or
+      // 7.1.2 continued
+      getOperator() = "-" and
+      exists(Boolean sign |
+        exprMayEqualInfinity(getLeftOperand(), sign) and
+        exprMayEqualInfinity(getRightOperand(), sign)
+      ) and
+      reason = "from subtraction of an infinity from itself"
+      or
+      // 7.1.3: multiplication of zero by infinity
+      getOperator() = "*" and
+      exprMayEqualZero(getAnOperand()) and
+      exprMayEqualInfinity(getAnOperand(), _) and
+      reason = "from multiplication of zero by infinity"
+      or
+      // 7.1.4: Division of zero by zero, or infinity by infinity
+      getOperator() = "/" and
+      exprMayEqualZero(getLeftOperand()) and
+      exprMayEqualZero(getRightOperand()) and
+      reason = "from division of zero by zero"
+      or
+      // 7.1.4 continued
+      getOperator() = "/" and
+      exprMayEqualInfinity(getLeftOperand(), _) and
+      exprMayEqualInfinity(getRightOperand(), _) and
+      reason = "from division of infinity by infinity"
+      or
+      // 7.1.5: x % y where y is zero or x is infinite
+      getOperator() = "%" and
+      exprMayEqualInfinity(getLeftOperand(), _) and
+      reason = "from modulus of infinity"
+      or
+      // 7.1.5 continued
+      getOperator() = "%" and
+      exprMayEqualZero(getRightOperand()) and
+      reason = "from modulus by zero"
+      // 7.1.6 handles the sqrt function, not covered here.
+      // 7.1.7 declares exceptions during invalid conversions, which we catch as sinks in our flow
+      // analysis.
+      // 7.1.8 declares exceptions for unordered comparisons, which we catch as sinks in our flow
+      // analysis.
+    )
+  }
+
+  override string getReason() { result = reason }
+}
+
+module InvalidNaNUsage implements DataFlow::ConfigSig {
+  /**
+   * An expression which has non-NaN inputs and may produce a NaN output.
+   */
+  predicate isSource(DataFlow::Node node) {
+    potentialSource(node) and
+    not exists(DataFlow::Node prior |
+      isAdditionalFlowStep(prior, node) and
+      potentialSource(prior)
+    )
+  }
+
+  /**
+   * An expression which may produce a NaN output.
+   */
+  additional predicate potentialSource(DataFlow::Node node) {
+    node.asExpr() instanceof PotentiallyNaNExpr
+  }
+
+  predicate isBarrierOut(DataFlow::Node node) {
+    guardedNotFPClass(node.asExpr(), TNaN())
+    or
+    exists(Expr e |
+      e.getType() instanceof IntegralType and
+      e = node.asConvertedExpr()
+    )
+  }
+
+  /**
+   * Add an additional flow step to handle NaN propagation through floating point operations.
+   */
+  predicate isAdditionalFlowStep(DataFlow::Node source, DataFlow::Node sink) {
+    exists(Operation o |
+      o.getAnOperand() = source.asExpr() and
+      o = sink.asExpr() and
+      o.getType() instanceof FloatingPointType
+    )
+  }
+
+  predicate isSink(DataFlow::Node node) {
+    not guardedNotFPClass(node.asExpr(), TNaN()) and
+    node instanceof InvalidNaNUsage
+  }
+}
+
+class InvalidNaNUsage extends DataFlow::Node {
+  string description;
+  string nanDescription;
+
+  InvalidNaNUsage() {
+    // Case 1: NaNs shall not be compared, except to themselves
+    exists(ComparisonOperation cmp |
+      this.asExpr() = cmp.getAnOperand() and
+      not hashCons(cmp.getLeftOperand()) = hashCons(cmp.getRightOperand()) and
+      description = "Comparison involving a $@, which always evaluates to false." and
+      nanDescription = "possibly NaN float value"
+    )
+    or
+    // Case 2: NaNs and infinities shall not be cast to integers
+    exists(Conversion c |
+      this.asExpr() = c.getUnconverted() and
+      c.getExpr().getType() instanceof FloatingPointType and
+      c.getType() instanceof IntegralType and
+      description = "$@ casted to integer." and
+      nanDescription = "Possibly NaN float value"
+    )
+  }
+
+  string getDescription() { result = description }
+
+  string getNaNDescription() { result = nanDescription }
+}
+
+module InvalidNaNFlow = DataFlow::Global<InvalidNaNUsage>;
+
+import InvalidNaNFlow::PathGraph
+
+from
+  Element elem, InvalidNaNFlow::PathNode source, InvalidNaNFlow::PathNode sink,
+  InvalidNaNUsage usage, Expr sourceExpr, string sourceString, Element extra, string extraString
+where
+  not InvalidNaNFlow::PathGraph::edges(_, source, _, _) and
+  not InvalidNaNFlow::PathGraph::edges(sink, _, _, _) and
+  not sourceExpr.isFromTemplateInstantiation(_) and
+  not usage.asExpr().isFromTemplateInstantiation(_) and
+  elem = MacroUnwrapper<Expr>::unwrapElement(sink.getNode().asExpr()) and
+  usage = sink.getNode() and
+  sourceExpr = source.getNode().asExpr() and
+  sourceString = " (" + source.getNode().asExpr().(PotentiallyNaNExpr).getReason() + ")" and
+  InvalidNaNFlow::flow(source.getNode(), usage) and
+  (
+    if not sourceExpr.getEnclosingFunction() = usage.asExpr().getEnclosingFunction()
+    then
+      extraString =
+        usage.getNaNDescription() + sourceString + " computed in function " +
+          sourceExpr.getEnclosingFunction().getName() and
+      extra = sourceExpr.getEnclosingFunction()
+    else (
+      extra = sourceExpr and
+      extraString = usage.getNaNDescription() + sourceString
+    )
+  )
+select elem, source, sink, usage.getDescription(), extra, extraString
diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected
new file mode 100644
index 000000000..f1f08b5a5
--- /dev/null
+++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.expected
@@ -0,0 +1,113 @@
+edges
+| test.c:8:14:8:20 | ... / ... | test.c:8:14:8:20 | ... / ... | provenance |  |
+| test.c:8:14:8:20 | ... / ... | test.c:9:14:9:16 | - ... | provenance | Config |
+| test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | provenance |  |
+| test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | provenance |  |
+| test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | provenance |  |
+| test.c:9:14:9:16 | - ... | test.c:9:14:9:16 | - ... | provenance |  |
+| test.c:9:14:9:16 | - ... | test.c:13:8:13:9 | l3 | provenance |  |
+| test.c:9:14:9:16 | - ... | test.c:19:3:19:9 | l3 | provenance |  |
+| test.c:9:14:9:16 | - ... | test.c:28:19:28:20 | l3 | provenance |  |
+| test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance |  |
+| test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:77:15:77:21 | ... / ... | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | provenance |  |
+| test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | provenance |  |
+| test.c:175:22:175:22 | p | test.c:175:27:175:32 | p | provenance |  |
+| test.c:183:34:183:34 | p | test.c:185:13:185:18 | p | provenance |  |
+| test.c:189:32:189:32 | p | test.c:189:47:189:59 | ... + ... | provenance | Config |
+| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:189:47:189:59 | ... + ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:189:51:189:59 | ... / ... | test.c:189:47:189:59 | ... + ... | provenance | Config |
+| test.c:193:13:194:15 | ... / ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:200:25:200:33 | ... / ... | test.c:183:34:183:34 | p | provenance |  |
+| test.c:204:19:204:27 | ... / ... | test.c:204:19:204:27 | ... / ... | provenance |  |
+| test.c:204:19:204:27 | ... / ... | test.c:206:21:206:31 | ... + ... | provenance | Config |
+| test.c:206:21:206:31 | ... + ... | test.c:206:21:206:31 | ... + ... | provenance |  |
+| test.c:206:21:206:31 | ... + ... | test.c:208:13:208:21 | middleInf | provenance |  |
+| test.c:206:21:206:31 | ... + ... | test.c:210:23:210:31 | middleInf | provenance |  |
+| test.c:208:13:208:21 | middleInf | test.c:175:22:175:22 | p | provenance |  |
+| test.c:210:23:210:31 | middleInf | test.c:189:32:189:32 | p | provenance |  |
+nodes
+| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
+| test.c:8:14:8:20 | ... / ... | semmle.label | ... / ... |
+| test.c:9:14:9:16 | - ... | semmle.label | - ... |
+| test.c:9:14:9:16 | - ... | semmle.label | - ... |
+| test.c:12:8:12:9 | l2 | semmle.label | l2 |
+| test.c:13:8:13:9 | l3 | semmle.label | l3 |
+| test.c:18:3:18:9 | l2 | semmle.label | l2 |
+| test.c:19:3:19:9 | l3 | semmle.label | l3 |
+| test.c:27:19:27:20 | l2 | semmle.label | l2 |
+| test.c:28:19:28:20 | l3 | semmle.label | l3 |
+| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
+| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
+| test.c:38:3:38:9 | l7 | semmle.label | l7 |
+| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... |
+| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... |
+| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... |
+| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... |
+| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... |
+| test.c:77:15:77:21 | ... / ... | semmle.label | ... / ... |
+| test.c:79:5:79:12 | l12 | semmle.label | l12 |
+| test.c:87:5:87:12 | l12 | semmle.label | l12 |
+| test.c:91:5:91:12 | l12 | semmle.label | l12 |
+| test.c:93:5:93:12 | l12 | semmle.label | l12 |
+| test.c:99:5:99:12 | l12 | semmle.label | l12 |
+| test.c:105:5:105:12 | l12 | semmle.label | l12 |
+| test.c:111:5:111:12 | l12 | semmle.label | l12 |
+| test.c:114:16:114:23 | l12 | semmle.label | l12 |
+| test.c:117:23:117:30 | l12 | semmle.label | l12 |
+| test.c:120:20:120:27 | l12 | semmle.label | l12 |
+| test.c:163:3:164:16 | ... / ... | semmle.label | ... / ... |
+| test.c:175:22:175:22 | p | semmle.label | p |
+| test.c:175:27:175:32 | p | semmle.label | p |
+| test.c:183:34:183:34 | p | semmle.label | p |
+| test.c:185:13:185:18 | p | semmle.label | p |
+| test.c:189:32:189:32 | p | semmle.label | p |
+| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... |
+| test.c:189:47:189:59 | ... + ... | semmle.label | ... + ... |
+| test.c:189:51:189:59 | ... / ... | semmle.label | ... / ... |
+| test.c:193:13:194:15 | ... / ... | semmle.label | ... / ... |
+| test.c:200:25:200:33 | ... / ... | semmle.label | ... / ... |
+| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... |
+| test.c:204:19:204:27 | ... / ... | semmle.label | ... / ... |
+| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... |
+| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... |
+| test.c:208:13:208:21 | middleInf | semmle.label | middleInf |
+| test.c:210:23:210:31 | middleInf | semmle.label | middleInf |
+subpaths
+#select
+| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
+| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
+| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | $@ casted to integer. | test.c:8:14:8:20 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
+| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Division operation may silently underflow and produce zero, as the divisor $@. | test.c:8:14:8:20 | ... / ... | may be an infinite float value from division by zero |
+| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | $@ casted to integer. | test.c:31:14:32:15 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | $@ casted to integer. | test.c:61:11:61:17 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | $@ casted to integer. | test.c:66:11:66:19 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | $@ casted to integer. | test.c:72:20:72:28 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | $@ casted to integer. | test.c:75:24:75:32 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | $@ casted to integer. | test.c:77:15:77:21 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:163:9:164:15 | ... / ... | test.c:163:3:164:16 | ... / ... | test.c:163:3:164:16 | ... / ... | $@ casted to integer. | test.c:163:9:164:15 | ... / ... | Possibly infinite float value from division by zero |
+| test.c:175:32:175:32 | p | test.c:189:51:189:59 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:189:6:189:24 | addInfThenCastToInt | Possibly infinite float value computed in function addInfThenCastToInt |
+| test.c:175:32:175:32 | p | test.c:193:13:194:15 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |
+| test.c:175:32:175:32 | p | test.c:204:19:204:27 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |
+| test.c:185:18:185:18 | p | test.c:200:25:200:33 | ... / ... | test.c:185:13:185:18 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly infinite float value computed in function f2 |
diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref
new file mode 100644
index 000000000..dccac37c5
--- /dev/null
+++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.qlref
@@ -0,0 +1 @@
+rules/DIR-4-15/PossibleMisuseOfUndetectedInfinity.ql
\ No newline at end of file
diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected
new file mode 100644
index 000000000..e0047d9ef
--- /dev/null
+++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.expected
@@ -0,0 +1,136 @@
+edges
+| test.c:27:14:27:20 | ... / ... | test.c:27:14:27:20 | ... / ... | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:36:3:36:9 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | provenance |  |
+| test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | provenance |  |
+| test.c:28:14:28:20 | ... / ... | test.c:28:14:28:20 | ... / ... | provenance |  |
+| test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | provenance |  |
+| test.c:28:14:28:20 | ... / ... | test.c:52:3:52:4 | l6 | provenance |  |
+| test.c:31:14:32:15 | ... / ... | test.c:31:14:32:15 | ... / ... | provenance |  |
+| test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | provenance |  |
+| test.c:31:14:32:15 | ... / ... | test.c:53:3:53:4 | l7 | provenance |  |
+| test.c:33:14:33:22 | ... / ... | test.c:33:14:33:22 | ... / ... | provenance |  |
+| test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | provenance |  |
+| test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:122:15:122:21 | ... / ... | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:155:20:155:27 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:157:23:157:30 | l13 | provenance |  |
+| test.c:122:15:122:21 | ... / ... | test.c:158:16:158:23 | l13 | provenance |  |
+| test.c:175:22:175:22 | p | test.c:175:27:175:32 | p | provenance |  |
+| test.c:183:34:183:34 | p | test.c:185:13:185:18 | p | provenance |  |
+| test.c:188:32:188:32 | p | test.c:188:47:188:51 | ... + ... | provenance | Config |
+| test.c:188:47:188:51 | ... + ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:190:32:190:32 | p | test.c:190:47:190:59 | ... + ... | provenance | Config |
+| test.c:190:47:190:59 | ... + ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:190:47:190:59 | ... + ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:190:51:190:59 | ... / ... | test.c:190:47:190:59 | ... + ... | provenance | Config |
+| test.c:195:13:195:21 | ... / ... | test.c:175:22:175:22 | p | provenance |  |
+| test.c:199:23:199:31 | ... / ... | test.c:188:32:188:32 | p | provenance |  |
+| test.c:201:25:201:33 | ... / ... | test.c:183:34:183:34 | p | provenance |  |
+| test.c:205:19:205:27 | ... / ... | test.c:205:19:205:27 | ... / ... | provenance |  |
+| test.c:205:19:205:27 | ... / ... | test.c:207:21:207:31 | ... + ... | provenance | Config |
+| test.c:207:21:207:31 | ... + ... | test.c:207:21:207:31 | ... + ... | provenance |  |
+| test.c:207:21:207:31 | ... + ... | test.c:209:13:209:21 | middleNaN | provenance |  |
+| test.c:207:21:207:31 | ... + ... | test.c:211:23:211:31 | middleNaN | provenance |  |
+| test.c:209:13:209:21 | middleNaN | test.c:175:22:175:22 | p | provenance |  |
+| test.c:211:23:211:31 | middleNaN | test.c:190:32:190:32 | p | provenance |  |
+nodes
+| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... |
+| test.c:27:14:27:20 | ... / ... | semmle.label | ... / ... |
+| test.c:28:14:28:20 | ... / ... | semmle.label | ... / ... |
+| test.c:28:14:28:20 | ... / ... | semmle.label | ... / ... |
+| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
+| test.c:31:14:32:15 | ... / ... | semmle.label | ... / ... |
+| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... |
+| test.c:33:14:33:22 | ... / ... | semmle.label | ... / ... |
+| test.c:36:3:36:9 | l5 | semmle.label | l5 |
+| test.c:37:3:37:9 | l6 | semmle.label | l6 |
+| test.c:38:3:38:9 | l7 | semmle.label | l7 |
+| test.c:39:3:39:9 | l8 | semmle.label | l8 |
+| test.c:46:3:46:4 | l5 | semmle.label | l5 |
+| test.c:47:3:47:4 | l5 | semmle.label | l5 |
+| test.c:48:3:48:4 | l5 | semmle.label | l5 |
+| test.c:49:3:49:4 | l5 | semmle.label | l5 |
+| test.c:50:3:50:4 | l5 | semmle.label | l5 |
+| test.c:51:3:51:4 | l5 | semmle.label | l5 |
+| test.c:52:3:52:4 | l6 | semmle.label | l6 |
+| test.c:53:3:53:4 | l7 | semmle.label | l7 |
+| test.c:54:3:54:4 | l8 | semmle.label | l8 |
+| test.c:61:5:61:18 | ... / ... | semmle.label | ... / ... |
+| test.c:66:5:66:20 | ... / ... | semmle.label | ... / ... |
+| test.c:72:14:72:29 | ... / ... | semmle.label | ... / ... |
+| test.c:75:18:75:33 | ... / ... | semmle.label | ... / ... |
+| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... |
+| test.c:122:15:122:21 | ... / ... | semmle.label | ... / ... |
+| test.c:126:5:126:12 | l13 | semmle.label | l13 |
+| test.c:132:5:132:12 | l13 | semmle.label | l13 |
+| test.c:138:5:138:12 | l13 | semmle.label | l13 |
+| test.c:144:5:144:12 | l13 | semmle.label | l13 |
+| test.c:148:5:148:12 | l13 | semmle.label | l13 |
+| test.c:155:20:155:27 | l13 | semmle.label | l13 |
+| test.c:157:23:157:30 | l13 | semmle.label | l13 |
+| test.c:158:16:158:23 | l13 | semmle.label | l13 |
+| test.c:166:3:166:18 | call to pow | semmle.label | call to pow |
+| test.c:171:3:171:15 | call to acos | semmle.label | call to acos |
+| test.c:175:22:175:22 | p | semmle.label | p |
+| test.c:175:27:175:32 | p | semmle.label | p |
+| test.c:183:34:183:34 | p | semmle.label | p |
+| test.c:185:13:185:18 | p | semmle.label | p |
+| test.c:188:32:188:32 | p | semmle.label | p |
+| test.c:188:47:188:51 | ... + ... | semmle.label | ... + ... |
+| test.c:190:32:190:32 | p | semmle.label | p |
+| test.c:190:47:190:59 | ... + ... | semmle.label | ... + ... |
+| test.c:190:47:190:59 | ... + ... | semmle.label | ... + ... |
+| test.c:190:51:190:59 | ... / ... | semmle.label | ... / ... |
+| test.c:195:13:195:21 | ... / ... | semmle.label | ... / ... |
+| test.c:199:23:199:31 | ... / ... | semmle.label | ... / ... |
+| test.c:201:25:201:33 | ... / ... | semmle.label | ... / ... |
+| test.c:205:19:205:27 | ... / ... | semmle.label | ... / ... |
+| test.c:205:19:205:27 | ... / ... | semmle.label | ... / ... |
+| test.c:207:21:207:31 | ... + ... | semmle.label | ... + ... |
+| test.c:207:21:207:31 | ... + ... | semmle.label | ... + ... |
+| test.c:209:13:209:21 | middleNaN | semmle.label | middleNaN |
+| test.c:211:23:211:31 | middleNaN | semmle.label | middleNaN |
+subpaths
+#select
+| test.c:36:8:36:9 | l5 | test.c:27:14:27:20 | ... / ... | test.c:36:3:36:9 | l5 | $@ casted to integer. | test.c:27:14:27:20 | ... / ... | Possibly NaN float value (from division of infinity by infinity) |
+| test.c:37:8:37:9 | l6 | test.c:28:14:28:20 | ... / ... | test.c:37:3:37:9 | l6 | $@ casted to integer. | test.c:28:14:28:20 | ... / ... | Possibly NaN float value (from division of infinity by infinity) |
+| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | $@ casted to integer. | test.c:31:14:32:15 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:39:8:39:9 | l8 | test.c:33:14:33:22 | ... / ... | test.c:39:3:39:9 | l8 | $@ casted to integer. | test.c:33:14:33:22 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:46:3:46:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:46:3:46:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:47:3:47:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:47:3:47:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:48:3:48:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:48:3:48:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:49:3:49:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:49:3:49:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:50:3:50:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:50:3:50:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:51:3:51:4 | l5 | test.c:27:14:27:20 | ... / ... | test.c:51:3:51:4 | l5 | Comparison involving a $@, which always evaluates to false. | test.c:27:14:27:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:52:3:52:4 | l6 | test.c:28:14:28:20 | ... / ... | test.c:52:3:52:4 | l6 | Comparison involving a $@, which always evaluates to false. | test.c:28:14:28:20 | ... / ... | possibly NaN float value (from division of infinity by infinity) |
+| test.c:53:3:53:4 | l7 | test.c:31:14:32:15 | ... / ... | test.c:53:3:53:4 | l7 | Comparison involving a $@, which always evaluates to false. | test.c:31:14:32:15 | ... / ... | possibly NaN float value (from division of zero by zero) |
+| test.c:54:3:54:4 | l8 | test.c:33:14:33:22 | ... / ... | test.c:54:3:54:4 | l8 | Comparison involving a $@, which always evaluates to false. | test.c:33:14:33:22 | ... / ... | possibly NaN float value (from division of zero by zero) |
+| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | $@ casted to integer. | test.c:61:11:61:17 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | $@ casted to integer. | test.c:66:11:66:19 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | $@ casted to integer. | test.c:72:20:72:28 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | $@ casted to integer. | test.c:75:24:75:32 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:126:10:126:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:126:5:126:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:132:10:132:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:132:5:132:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:138:10:138:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:138:5:138:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:144:10:144:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:144:5:144:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:148:10:148:12 | l13 | test.c:122:15:122:21 | ... / ... | test.c:148:5:148:12 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:155:25:155:27 | l13 | test.c:122:15:122:21 | ... / ... | test.c:155:20:155:27 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:157:28:157:30 | l13 | test.c:122:15:122:21 | ... / ... | test.c:157:23:157:30 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:158:21:158:23 | l13 | test.c:122:15:122:21 | ... / ... | test.c:158:16:158:23 | l13 | $@ casted to integer. | test.c:122:15:122:21 | ... / ... | Possibly NaN float value (from division of zero by zero) |
+| test.c:166:8:166:10 | call to pow | test.c:166:3:166:18 | call to pow | test.c:166:3:166:18 | call to pow | $@ casted to integer. | test.c:166:8:166:10 | call to pow | Possibly NaN float value (both arguments are equal to zero) |
+| test.c:171:8:171:11 | call to acos | test.c:171:3:171:15 | call to acos | test.c:171:3:171:15 | call to acos | $@ casted to integer. | test.c:171:8:171:11 | call to acos | Possibly NaN float value (the argument has a range -1000000000000000...1000000000000000 which is outside the domain of this function (-1.0...1.0)) |
+| test.c:175:32:175:32 | p | test.c:190:51:190:59 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:190:6:190:24 | addNaNThenCastToInt | Possibly NaN float value (from division of zero by zero) computed in function addNaNThenCastToInt |
+| test.c:175:32:175:32 | p | test.c:195:13:195:21 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 |
+| test.c:175:32:175:32 | p | test.c:199:23:199:31 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 |
+| test.c:175:32:175:32 | p | test.c:205:19:205:27 | ... / ... | test.c:175:27:175:32 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 |
+| test.c:185:18:185:18 | p | test.c:201:25:201:33 | ... / ... | test.c:185:13:185:18 | p | $@ casted to integer. | test.c:192:6:192:7 | f2 | Possibly NaN float value (from division of zero by zero) computed in function f2 |
diff --git a/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref
new file mode 100644
index 000000000..d88c172bd
--- /dev/null
+++ b/c/misra/test/rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.qlref
@@ -0,0 +1 @@
+rules/DIR-4-15/PossibleMisuseOfUndetectedNaN.ql
\ No newline at end of file
diff --git a/c/misra/test/rules/DIR-4-15/test.c b/c/misra/test/rules/DIR-4-15/test.c
new file mode 100644
index 000000000..a827a7df9
--- /dev/null
+++ b/c/misra/test/rules/DIR-4-15/test.c
@@ -0,0 +1,212 @@
+#include "math.h"
+
+float getFloat() { return 1.0; }
+
+// Parameter could be infinity
+void f1(float p1) {
+  float l1 = 1;
+  float l2 = 1.0 / 0;
+  float l3 = -l2;
+
+  10 / l1;         // COMPLIANT
+  10 / l2;         // NON_COMPLIANT: Underflows to zero
+  10 / l3;         // NON_COMPLIANT: Underflow to negative zero
+  10 / p1;         // COMPLIANT: Reduce false positives by assuming not infinity
+  10 / getFloat(); // COMPLIANT: Reduce false positives by assuming not infinity
+
+  (int)l1;         // COMPLIANT
+  (int)l2;         // NON_COMPLIANT
+  (int)l3;         // NON_COMPLIANT
+  (int)p1;         // COMPLIANT: Reduce false positives by assuming not infinity
+  (int)getFloat(); // COMPLIANT: Reduce false positives by assuming not infinity
+
+  // Not NaN:
+  float l4 = l1 / l1; // COMPLIANT
+
+  // NaN because of infinity divided by itself:
+  float l5 = l2 / l2; // NON_COMPLIANT: Division by infinity not allowed.
+  float l6 = l3 / l3; // NON_COMPLIANT: Division by infinity not allowed.
+
+  // NaN because of zero divided by itself:
+  float l7 = getFloat() /
+             p1; // COMPLIANT: Reduce false positives by assuming not infinity
+  float l8 = 0.0 / 0.0;
+
+  (int)l4; // COMPLIANT
+  (int)l5; // NON_COMPLIANT: Casting NaN to int
+  (int)l6; // NON_COMPLIANT: Casting NaN to int
+  (int)l7; // NON_COMPLIANT: Casting NaN to int
+  (int)l8; // NON_COMPLIANT: Casting NaN to int
+
+  l4 == 0; // COMPLIANT
+  l4 != 0; // COMPLIANT
+  l4 <= 0; // COMPLIANT
+  l4 < 0;  // COMPLIANT
+  l4 >= 0; // COMPLIANT
+  l5 == 0; // NON_COMPLIANT: Comparison with NaN always false
+  l5 != 0; // NON_COMPLIANT: Comparison with NaN always false
+  l5 < 0;  // NON_COMPLIANT: Comparison with NaN always false
+  l5 <= 0; // NON_COMPLIANT: Comparison with NaN always false
+  l5 > 0;  // NON_COMPLIANT: Comparison with NaN always false
+  l5 >= 0; // NON_COMPLIANT: Comparison with NaN always false
+  l6 == 0; // NON_COMPLIANT: Comparison with NaN always false
+  l7 == 0; // NON_COMPLIANT: Comparison with NaN always false
+  l8 == 0; // NON_COMPLIANT: Comparison with NaN always false
+
+  // Guards
+  float l9 = 0;
+  if (l9 != 0) {
+    (int)(l9 / l9); // COMPLIANT: l9 is not zero
+  } else {
+    (int)(l9 / l9); // NON_COMPLIANT: Guarded to not be NaN
+  }
+
+  float l10 = 0;
+  if (l10 == 0) {
+    (int)(l10 / l10); // NON_COMPLIANT: Casting NaN to integer
+  } else {
+    (int)(l10 / l10); // COMPLIANT: Guarded to not be NaN
+  }
+
+  float l11 = 0;
+  l11 == 0 ? (int)(l11 / l11) : 0; // NON_COMPLIANT
+  l11 == 0 ? 0 : (int)(l11 / l11); // COMPLIANT
+  l11 != 0 ? (int)(l11 / l11) : 0; // COMPLIANT
+  l11 != 0 ? 0 : (int)(l11 / l11); // NON_COMPLIANT
+
+  float l12 = 1.0 / 0;
+  if (isinf(l12)) {
+    (int)l12; // NON_COMPLIANT: Casting Infinity to integer
+  } else {
+    (int)l12; // COMPLIANT: Guarded not to be Infinity
+  }
+
+  if (!isinf(l12)) {
+    (int)l12; // COMPLIANT: Guarded not to be Infinity
+  } else {
+    (int)l12; // NON_COMPLIANT: Casting Infinity to integer
+  }
+
+  if (isinf(l12) == 1) {
+    (int)l12; // NON_COMPLIANT: Must be +Infinity
+  } else {
+    (int)l12; // NON_COMPLIANT: May be -Infinity
+  }
+
+  if (isfinite(l12)) {
+    (int)l12; // COMPLIANT: Guarded not to be Infinity
+  } else {
+    (int)l12; // NON_COMPLIANT: Casting Infinity to integer
+  }
+
+  if (isnormal(l12)) {
+    (int)l12; // COMPLIANT: Guarded not to be Infinity
+  } else {
+    (int)l12; // NON_COMPLIANT: Casting Infinity to integer
+  }
+
+  if (isnan(l12)) {
+    (int)l12; // COMPLIANT: Guarded not to be Infinity
+  } else {
+    (int)l12; // NON_COMPLIANT: Casting Infinity to integer
+  }
+
+  isinf(l12) ? (int)l12 : 0;    // NON_COMPLIANT: Check on wrong branch
+  isinf(l12) ? 0 : (int)l12;    // COMPLIANT: Checked not infinite before use
+  isfinite(l12) ? (int)l12 : 0; // COMPLIANT: Checked finite before use
+  isfinite(l12) ? 0 : (int)l12; // NON_COMPLIANT: Checked on wrong branch
+  isnan(l12) ? (int)l12
+             : 0; // COMPLIANT: Checked NaN, therefore not infinite, before use
+  isnan(l12) ? 0 : (int)l12; // NON_COMPLIANT: Check on wrong branch
+
+  float l13 = 0.0 / 0;
+  if (isinf(l13)) {
+    (int)l13; // COMPLIANT: Guarded not to be NaN
+  } else {
+    (int)l13; // NON_COMPLIANT: Casting NaN to integer
+  }
+
+  if (isinf(l13) == 1) {
+    (int)l13; // COMPLIANT: Guarded not to be NaN (must be +Infinity)
+  } else {
+    (int)l13; // NON_COMPLIANT: Casting NaN to integer
+  }
+
+  if (isfinite(l13)) {
+    (int)l13; // COMPLIANT: Guarded not to be NaN
+  } else {
+    (int)l13; // NON_COMPLIANT: Casting NaN to integer
+  }
+
+  if (isnormal(l13)) {
+    (int)l13; // COMPLIANT: Guarded not to be NaN
+  } else {
+    (int)l13; // NON_COMPLIANT: Casting NaN to integer
+  }
+
+  if (isnan(l13)) {
+    (int)l13; // NON_COMPLIANT: Casting NaN to integer
+  } else {
+    (int)l13; // COMPLIANT: Guarded not to be NaN
+  }
+
+  isinf(l13) ? (int)l13
+             : 0; // COMPLIANT: Checked infinite, therefore not NaN, before use
+  isinf(l13) ? 0 : (int)l13;    // COMPLIANT: Check on wrong branch
+  isfinite(l13) ? (int)l13 : 0; // COMPLIANT: Checked finite before use
+  isfinite(l13) ? 0 : (int)l13; // NON_COMPLIANT: Checked on wrong branch
+  isnan(l13) ? (int)l13 : 0;    // NON_COMPLIANT: Check on wrong branch
+  isnan(l13) ? 0 : (int)l13;    // COMPLIANT: Checked not NaN before use
+
+  (int)pow(2, p1);      // NON_COMPLIANT: likely to be Infinity
+  (int)pow(2, sin(p1)); // COMPLIANT: not likely to be Infinity
+  (int)(1 /
+        sin(p1)); // NON_COMPLIANT: possible infinity from zero in denominator
+  (int)(1 / log(p1)); // COMPLIANT: not possibly zero in denominator
+  (int)pow(p1, p1);   // NON_COMPLIANT: NaN if p1 is zero
+  if (p1 != 0) {
+    (int)pow(p1, p1); // COMPLIANT: p1 is not zero
+  }
+
+  (int)acos(p1);      // NON_COMPLIANT: NaN if p1 is not within -1..1
+  (int)acos(cos(p1)); // COMPLIANT: cos(p1) is within -1..1
+}
+
+void castToInt(float p) { (int)p; }
+
+void checkBeforeCastToInt(float p) {
+  if (isfinite(p)) {
+    castToInt(p);
+  }
+}
+
+void castToIntToFloatToInt(float p) {
+  // This should be reported as a violation, but not downstream from here.
+  castToInt((int)p);
+}
+
+void addOneThenCastToInt(float p) { castToInt(p + 1); }
+void addInfThenCastToInt(float p) { castToInt(p + 1.0 / 0.0); }
+void addNaNThenCastToInt(float p) { castToInt(p + 0.0 / 0.0); }
+
+void f2() {
+  castToInt(1.0 /
+            0.0); // NON_COMPLIANT: Infinity flows to denominator in division
+  castToInt(0.0 / 0.0); // NON_COMPLIANT: NaN flows to denominator in division
+  checkBeforeCastToInt(1.0 / 0.0);  // COMPLIANT
+  checkBeforeCastToInt(0.0 / 0.0);  // COMPLIANT
+  addOneThenCastToInt(1.0 / 0.0);   // NON_COMPLIANT[False negative]
+  addOneThenCastToInt(0.0 / 0.0);   // NON_COMPLIANT
+  castToIntToFloatToInt(1.0 / 0.0); // NON_COMPLIANT
+  castToIntToFloatToInt(0.0 / 0.0); // NON_COMPLIANT
+
+  // Check that during flow analysis, we only report the true root cause:
+  float rootInf = 1.0 / 0.0;
+  float rootNaN = 0.0 / 0.0;
+  float middleInf = rootInf + 1;
+  float middleNaN = rootNaN + 1;
+  castToInt(middleInf);           // NON_COMPLIANT
+  castToInt(middleNaN);           // NON_COMPLIANT
+  addInfThenCastToInt(middleInf); // NON_COMPLIANT
+  addNaNThenCastToInt(middleNaN); // NON_COMPLIANT
+}
\ No newline at end of file
diff --git a/cpp/common/src/codingstandards/cpp/FloatingPoint.qll b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll
new file mode 100644
index 000000000..f3ba8dba1
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/FloatingPoint.qll
@@ -0,0 +1,342 @@
+import codeql.util.Boolean
+import codingstandards.cpp.RestrictedRangeAnalysis
+
+predicate exprMayEqualZero(Expr e) {
+  RestrictedRangeAnalysis::upperBound(e) >= 0 and
+  RestrictedRangeAnalysis::lowerBound(e) <= 0 and
+  not guardedNotEqualZero(e)
+}
+
+newtype TFPClassification =
+  TFinite() or
+  TNaN() or
+  TInfinite()
+
+class FPClassification extends TFPClassification {
+  string toString() {
+    this = TFinite() and
+    result = "finite"
+    or
+    this = TNaN() and
+    result = "NaN"
+    or
+    this = TInfinite() and
+    result = "infinite"
+  }
+}
+
+newtype TFPClassificationConstraint =
+  /* The value may be infinite, NaN, or finite. */
+  TUnclassified() or
+  /**
+   * The value must be one of: infinite, NaN, or finite.
+   *
+   * If strict is `true` then this inverts naively. For example, `!isfinite(x)` means `x` must not
+   * be finite. However, `!iszero(x)` is true for some finite values, and inverts to
+   * `TUnclassified`.
+   */
+  TExactFPClassification(TFPClassification cls, Boolean strict) or
+  /* The value must not be one of: infinite, NaN, or finite. */
+  TExcludeFPClassification(TFPClassification cls1)
+
+class FPClassificationConstraint extends TFPClassificationConstraint {
+  string toString() {
+    this = TUnclassified() and
+    result = "unclassified"
+    or
+    exists(FPClassification cls, Boolean strict |
+      this = TExactFPClassification(cls, strict) and
+      result = "must be " + cls.toString() + ", strict: " + strict.toString()
+      or
+      this = TExcludeFPClassification(cls) and
+      result = "must NOT be " + cls.toString()
+    )
+  }
+
+  /**
+   * Invert the constraint, for instance, "must be finite" becomes "must not be finite".
+   *
+   * Non-strict exact constraints are inverted to the unclassified constraint. For example,
+   * `iszero(x)` guarantees `x` to be finite, however, `!iszero(x)` can be true for all three
+   * classes of floating point values.
+   *
+   * The unclassified constraint inverts to itself.
+   */
+  FPClassificationConstraint invert() {
+    // Unclassified inverts to itself.
+    this = TUnclassified() and result = this
+    or
+    exists(FPClassification cls |
+      // `!isfinite()` implies is infinite or NaN.
+      this = TExactFPClassification(cls, true) and
+      result = TExcludeFPClassification(cls)
+      or
+      // `!iszero()` implies nothing.
+      this = TExactFPClassification(cls, false) and
+      result = TUnclassified()
+      or
+      // For completeness: `!isfinite(x) ? ... : x` would imply `isfinite(x)`.
+      this = TExcludeFPClassification(cls) and
+      result = TExactFPClassification(cls, true)
+    )
+  }
+
+  /**
+   * Naively invert the constraint, for instance, "must be finite" becomes "must not be finite".
+   *
+   * Word of caution: inverting a guard condition does not necessarily invert the constraint. For
+   * example, `iszero(x)` guarantees `x` to be finite, however, `isnotzero(x)` does not guarantee
+   * `x` not to be finite.
+   *
+   * The unclassified constraint is not inverted.
+   */
+  FPClassificationConstraint naiveInversion() {
+    this = TUnclassified() and result = this
+    or
+    exists(FPClassification cls |
+      this = TExactFPClassification(cls, _) and
+      result = TExcludeFPClassification(cls)
+      or
+      this = TExcludeFPClassification(cls) and
+      result = TExactFPClassification(cls, true)
+    )
+  }
+
+  predicate mustBe(FPClassification cls) { this = TExactFPClassification(cls, _) }
+
+  predicate mustNotBe(FPClassification cls) {
+    this = TExcludeFPClassification(cls)
+    or
+    this = TExactFPClassification(_, _) and
+    not this = TExactFPClassification(cls, _)
+  }
+
+  predicate mayBe(FPClassification cls) { not mustNotBe(cls) }
+}
+
+/**
+ * The names of the functions or macros that classify floating point values.
+ *
+ * These names reflect a check that a value is finite, or infinite, or NaN. Finite and NaN checks
+ * are either strict (return true for all values in the class) or not (return true for some
+ * values).
+ *
+ * The infinite check is always strict, and specially, returns 1 or -1 for positive or negative
+ * infinity.
+ */
+newtype TFPClassifierName =
+  TClassifiesFinite(string name, boolean strict) {
+    strict = true and
+    name = ["finite" + ["", "l", "f"], "isfinite"]
+    or
+    strict = false and
+    name = ["isnormal", "issubnormal", "iszero"]
+  } or
+  TClassifiesNaN(string name, boolean strict) {
+    strict = true and
+    name = "isnan" + ["", "f", "l"]
+    or
+    strict = false and
+    name = "issignaling"
+  } or
+  TClassifiesInfinite(string name) { name = "isinf" + ["", "f", "l"] }
+
+class FPClassifierName extends TFPClassifierName {
+  string name;
+  boolean strict;
+
+  FPClassifierName() {
+    this = TClassifiesFinite(name, strict)
+    or
+    this = TClassifiesInfinite(name) and
+    strict = true
+    or
+    this = TClassifiesNaN(name, strict)
+  }
+
+  string toString() { result = name }
+
+  /** The classification name, for instance, "isfinite". */
+  string getName() { result = name }
+
+  /**
+   * Whether the check holds for all values in the class, or only some.
+   *
+   * For instance, "isfinite" is strict because it returns true for all finite values, but
+   * "isnormal" is not as it returns false for some finite values.
+   */
+  predicate isStrict() { strict = true }
+
+  FPClassificationConstraint getConstraint() {
+    this = TClassifiesFinite(_, strict) and
+    result = TExactFPClassification(any(TFinite t), strict)
+    or
+    this = TClassifiesNaN(_, strict) and
+    result = TExactFPClassification(any(TNaN t), strict)
+    or
+    this = TClassifiesInfinite(_) and
+    // TODO: isinf() is special
+    result = TExactFPClassification(any(TInfinite t), false)
+  }
+}
+
+/**
+ * An invocation of a classification function, for instance, "isfinite(x)", implemented as a macro.
+ */
+class FPClassifierMacroInvocation extends MacroInvocation {
+  FPClassifierName classifier;
+
+  FPClassifierMacroInvocation() { getMacroName() = classifier.getName() }
+
+  Expr getCheckedExpr() {
+    // Getting the checked expr in a cross-platform way is extroardinarily difficult, as glibc has
+    // multiple conditional implementations of the same macro. Assume the checked expr is a
+    // variable access so we can search optimistically like so:
+    exists(VariableAccess va |
+      va.getTarget().getName() = getExpandedArgument(0) and
+      va = getAnExpandedElement() and
+      result = va
+    )
+  }
+
+  /**
+   * The classification name, for instance, "isfinite".
+   */
+  FPClassifierName getFPClassifierName() { result = classifier }
+}
+
+/**
+ * A classification function, for instance, "isfinite", when implemented as a function.
+ */
+class FPClassifierFunction extends Function {
+  FPClassifierName classifier;
+
+  FPClassifierFunction() { getName() = classifier.getName() }
+
+  FPClassifierName getFPClassifierName() { result = classifier }
+}
+
+class FPClassificationGuard instanceof GuardCondition {
+  Expr floatExpr;
+  Expr checkResultExpr;
+  FPClassifierName classifier;
+
+  FPClassificationGuard() {
+    super.comparesEq(checkResultExpr, _, _, _) and
+    (
+      exists(FPClassifierMacroInvocation m |
+        floatExpr = m.getCheckedExpr() and
+        checkResultExpr = m.getExpr() and
+        classifier = m.getFPClassifierName()
+      )
+      or
+      exists(FunctionCall fc, FPClassifierFunction f |
+        fc.getTarget() = f and
+        floatExpr = fc.getArgument(0) and
+        checkResultExpr = fc and
+        classifier = f.getFPClassifierName()
+      )
+    )
+  }
+
+  string toString() {
+    result =
+      classifier.toString() + " guard on " + floatExpr.toString() + " via " +
+        checkResultExpr.toString()
+  }
+
+  predicate constrainsFPClass(Expr e, FPClassificationConstraint constraint, Boolean testIsTrue) {
+    floatExpr = e and
+    exists(BooleanValue value, boolean areEqual, int testResult, FPClassificationConstraint base |
+      super.comparesEq(checkResultExpr, testResult, areEqual, value) and
+      base = getBaseConstraint(areEqual, testResult) and
+      if value.getValue() = testIsTrue then constraint = base else constraint = base.invert()
+    )
+  }
+
+  // Helper function, gets base constraint assuming `classifier() == value` or `classifier != value`.
+  private FPClassificationConstraint getBaseConstraint(Boolean areEqual, int testResult) {
+    exists(FPClassificationConstraint base |
+      testResult = 0 and
+      exists(Boolean strict |
+        // Handle isfinite() != 0:
+        classifier = TClassifiesFinite(_, strict) and
+        base = TExactFPClassification(TFinite(), strict)
+        or
+        // Handle isNaN() != 0:
+        classifier = TClassifiesNaN(_, strict) and
+        base = TExactFPClassification(TNaN(), strict)
+        or
+        // Handle isinf() != 0, which matches for +/- infinity:
+        classifier = TClassifiesInfinite(_) and
+        base = TExactFPClassification(TInfinite(), true)
+      ) and
+      // Invert the base constraint in the case of `classifier() == 0`
+      if areEqual = false then result = base else result = base.invert()
+      or
+      // Handle isinf() == 1 or isInf() == -1, which matches for one of +/- infinity:
+      testResult = 1 and
+      classifier = TClassifiesInfinite(_) and
+      base = TExactFPClassification(TInfinite(), false) and
+      // Invert the base constraint in the case of `classifier() != 1`
+      if areEqual = true then result = base else result = base.invert()
+      // TODO: handle fpclassify() == FP_INFINITE, FP_NAN, FP_NORMAL, FP_ZERO, etc.
+    )
+  }
+
+  predicate controls(Expr e, boolean testIsTrue) {
+    exists(IRGuardCondition irg, IRBlock irb, Instruction eir, BooleanValue bval |
+      irg.getUnconvertedResultExpression() = this and
+      bval.getValue() = testIsTrue and
+      irg.valueControls(irb, bval) and
+      eir.getAst().(ControlFlowNode).getBasicBlock() = e.getBasicBlock() and
+      eir.getBlock() = irb
+    )
+  }
+}
+
+predicate guardedNotEqualZero(Expr e) {
+  /* Note Boolean cmpEq, false means cmpNeq */
+  exists(Expr checked, GuardCondition guard, boolean cmpEq, BooleanValue value |
+    hashCons(checked) = hashCons(e) and
+    guard.controls(e.getBasicBlock(), cmpEq) and
+    value.getValue() = cmpEq and
+    guard.comparesEq(checked, 0, false, value)
+  )
+  or
+  exists(Expr checked, Expr val, int valVal, GuardCondition guard, boolean cmpEq |
+    hashCons(checked) = hashCons(e) and
+    forex(float v |
+      v = [RestrictedRangeAnalysis::lowerBound(val), RestrictedRangeAnalysis::upperBound(val)]
+    |
+      valVal = v
+    ) and
+    guard.controls(e.getBasicBlock(), cmpEq) and
+    guard.comparesEq(checked, val, -valVal, false, cmpEq)
+  )
+}
+
+predicate guardedNotFPClass(Expr e, FPClassification cls) {
+  /* Note Boolean cmpEq, false means cmpNeq */
+  exists(
+    Expr checked, FPClassificationGuard guard, FPClassificationConstraint constraint, boolean cmpEq
+  |
+    hashCons(checked) = hashCons(e) and
+    guard.controls(e, cmpEq) and
+    guard.constrainsFPClass(checked, constraint, cmpEq) and
+    constraint.mustNotBe(cls)
+  )
+}
+
+predicate exprMayEqualInfinity(Expr e, Boolean positive) {
+  exists(float target |
+    positive = true and target = 1.0 / 0.0
+    or
+    positive = false and target = -1.0 / 0.0
+  |
+    RestrictedRangeAnalysis::upperBound(e.getUnconverted()) = target or
+    RestrictedRangeAnalysis::lowerBound(e.getUnconverted()) = target
+  ) and
+  not guardedNotFPClass(e, TInfinite()) and
+  not e.getType() instanceof IntegralType
+}
diff --git a/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll
new file mode 100644
index 000000000..b81f11328
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/RestrictedRangeAnalysis.qll
@@ -0,0 +1,2222 @@
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.HashCons
+
+/**
+ * A fork of SimpleRangeAnalysis.qll, which is intended to only give
+ * results with a conservative basis.
+ *
+ * For instance, since range analysis is local, a function call (e.g.
+ * `f()`) is given the widest possible range in the original library. In
+ * this fork, we do not provide any result.
+ *
+ * Original library level doc comment from SimpleRangeAnalysis.qll:
+ *
+ * Simple range analysis library. Range analysis is usually done as an
+ * abstract interpretation over the lattice of range values. (A range is a
+ * pair, containing a lower and upper bound for the value.) The problem
+ * with this approach is that the lattice is very tall, which means it can
+ * take an extremely large number of iterations to find the least fixed
+ * point. This example illustrates the problem:
+ *
+ *    int count = 0;
+ *    for (; p; p = p->next) {
+ *      count = count+1;
+ *    }
+ *
+ * The range of 'count' is initially (0,0), then (0,1) on the second
+ * iteration, (0,2) on the third iteration, and so on until we eventually
+ * reach maxInt.
+ *
+ * This library uses a crude solution to the problem described above: if
+ * the upper (or lower) bound of an expression might depend recursively on
+ * itself then we round it up (down for lower bounds) to one of a fixed set
+ * of values, such as 0, 1, 2, 256, and +Inf. This limits the height of the
+ * lattice which ensures that the analysis will terminate in a reasonable
+ * amount of time. This solution is similar to the abstract interpretation
+ * technique known as 'widening', but it is less precise because we are
+ * unable to inspect the bounds from the previous iteration of the fixed
+ * point computation. For example, widening might be able to deduce that
+ * the lower bound is -11 but we would approximate it to -16.
+ *
+ * QL does not allow us to compute an aggregate over a recursive
+ * sub-expression, so we cannot compute the minimum lower bound and maximum
+ * upper bound during the recursive phase of the query. Instead, the
+ * recursive phase computes a set of lower bounds and a set of upper bounds
+ * for each expression. We compute the minimum lower bound and maximum
+ * upper bound after the recursion is finished. This is another reason why
+ * we need to limit the number of bounds per expression, because they will
+ * all be stored until the recursive phase is finished.
+ *
+ * The ranges are represented using a pair of floating point numbers. This
+ * is simpler than using integers because floating point numbers cannot
+ * overflow and wrap. It is also convenient because we can detect overflow
+ * and negative overflow by looking for bounds that are outside the range
+ * of the type.
+ */
+module RestrictedRangeAnalysis {
+  import cpp
+  private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils as Util
+  import semmle.code.cpp.rangeanalysis.RangeSSA
+  import SimpleRangeAnalysisCached
+  private import semmle.code.cpp.rangeanalysis.NanAnalysis
+
+  float largeValue() { result = 1000000000000000.0 }
+
+  /**
+   * This fixed set of lower bounds is used when the lower bounds of an
+   * expression are recursively defined. The inferred lower bound is rounded
+   * down to the nearest lower bound in the fixed set. This restricts the
+   * height of the lattice, which prevents the analysis from exploding.
+   *
+   * Note: these bounds were chosen fairly arbitrarily. Feel free to add more
+   * 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
+    result = -largeValue() or
+    result = Util::typeLowerBound(t)
+    //result = max(float v | v = Util::typeLowerBound(t) or v = -largeValue())
+  }
+
+  /** 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
+    result = largeValue() or
+    result = Util::typeUpperBound(t)
+    //result = min(float v | v = Util::typeLowerBound(t) or v = largeValue())
+  }
+
+  /**
+   * Gets the value of the expression `e`, if it is a constant.
+   * This predicate also handles the case of constant variables initialized in different
+   * compilation units, which doesn't necessarily have a getValue() result from the extractor.
+   */
+  private string getValue(Expr e) {
+    if exists(e.getValue())
+    then result = e.getValue()
+    else
+      /*
+       * It should be safe to propagate the initialization value to a variable if:
+       * The type of v is const, and
+       * The type of v is not volatile, and
+       * Either:
+       *   v is a local/global variable, or
+       *   v is a static member variable
+       */
+
+      exists(VariableAccess access, StaticStorageDurationVariable v |
+        not v.getUnderlyingType().isVolatile() and
+        v.getUnderlyingType().isConst() and
+        e = access and
+        v = access.getTarget() and
+        result = getValue(v.getAnAssignedValue())
+      )
+  }
+
+  private float varMaxVal(Variable v) {
+    result = min(float f | f = Util::varMaxVal(v) or f = largeValue())
+  }
+
+  private float varMinVal(Variable v) {
+    result = max(float f | f = Util::varMinVal(v) or f = -largeValue())
+  }
+
+  private float exprMaxVal(Expr e) {
+    result = min(float f | f = Util::exprMaxVal(e) or f = largeValue())
+  }
+
+  private float exprMinVal(Expr e) {
+    result = max(float f | f = Util::exprMinVal(e) or f = -largeValue())
+  }
+
+  /**
+   * A bitwise `&` expression in which both operands are unsigned, or are effectively
+   * unsigned due to being a non-negative constant.
+   */
+  private class UnsignedBitwiseAndExpr extends BitwiseAndExpr {
+    UnsignedBitwiseAndExpr() {
+      (
+        this.getLeftOperand()
+            .getFullyConverted()
+            .getType()
+            .getUnderlyingType()
+            .(IntegralType)
+            .isUnsigned() or
+        getValue(this.getLeftOperand().getFullyConverted()).toInt() >= 0
+      ) and
+      (
+        this.getRightOperand()
+            .getFullyConverted()
+            .getType()
+            .getUnderlyingType()
+            .(IntegralType)
+            .isUnsigned() or
+        getValue(this.getRightOperand().getFullyConverted()).toInt() >= 0
+      )
+    }
+  }
+
+  /**
+   * Gets the floor of `v`, with additional logic to work around issues with
+   * large numbers.
+   */
+  bindingset[v]
+  float safeFloor(float v) {
+    // return the floor of v
+    v.abs() < 2.pow(31) and
+    result = v.floor()
+    or
+    // `floor()` doesn't work correctly on large numbers (since it returns an integer),
+    // so fall back to unrounded numbers at this scale.
+    not v.abs() < 2.pow(31) and
+    result = v
+  }
+
+  /** A `MulExpr` where exactly one operand is constant. */
+  private class MulByConstantExpr extends MulExpr {
+    float constant;
+    Expr operand;
+
+    MulByConstantExpr() {
+      exists(Expr constantExpr |
+        this.hasOperands(constantExpr, operand) and
+        constant = getValue(constantExpr.getFullyConverted()).toFloat() and
+        not exists(getValue(operand.getFullyConverted()).toFloat())
+      )
+    }
+
+    /** Gets the value of the constant operand. */
+    float getConstant() { result = constant }
+
+    /** Gets the non-constant operand. */
+    Expr getOperand() { result = operand }
+  }
+
+  private class UnsignedMulExpr extends MulExpr {
+    UnsignedMulExpr() {
+      this.getType().(IntegralType).isUnsigned() and
+      // Avoid overlap. It should be slightly cheaper to analyze
+      // `MulByConstantExpr`.
+      not this instanceof MulByConstantExpr
+    }
+  }
+
+  /**
+   * Holds if `expr` is effectively a multiplication of `operand` with the
+   * positive constant `positive`.
+   */
+  private predicate effectivelyMultipliesByPositive(Expr expr, Expr operand, float positive) {
+    operand = expr.(MulByConstantExpr).getOperand() and
+    positive = expr.(MulByConstantExpr).getConstant() and
+    positive >= 0.0 // includes positive zero
+    or
+    operand = expr.(UnaryPlusExpr).getOperand() and
+    positive = 1.0
+    or
+    operand = expr.(CommaExpr).getRightOperand() and
+    positive = 1.0
+    or
+    operand = expr.(StmtExpr).getResultExpr() and
+    positive = 1.0
+  }
+
+  /**
+   * Holds if `expr` is effectively a multiplication of `operand` with the
+   * negative constant `negative`.
+   */
+  private predicate effectivelyMultipliesByNegative(Expr expr, Expr operand, float negative) {
+    operand = expr.(MulByConstantExpr).getOperand() and
+    negative = expr.(MulByConstantExpr).getConstant() and
+    negative < 0.0 // includes negative zero
+    or
+    operand = expr.(UnaryMinusExpr).getOperand() and
+    negative = -1.0
+  }
+
+  private class AssignMulByConstantExpr extends AssignMulExpr {
+    float constant;
+
+    AssignMulByConstantExpr() {
+      constant = getValue(this.getRValue().getFullyConverted()).toFloat()
+    }
+
+    float getConstant() { result = constant }
+  }
+
+  private class AssignMulByPositiveConstantExpr extends AssignMulByConstantExpr {
+    AssignMulByPositiveConstantExpr() { constant >= 0.0 }
+  }
+
+  private class AssignMulByNegativeConstantExpr extends AssignMulByConstantExpr {
+    AssignMulByNegativeConstantExpr() { constant < 0.0 }
+  }
+
+  private class UnsignedAssignMulExpr extends AssignMulExpr {
+    UnsignedAssignMulExpr() {
+      this.getType().(IntegralType).isUnsigned() and
+      // Avoid overlap. It should be slightly cheaper to analyze
+      // `AssignMulByConstantExpr`.
+      not this instanceof AssignMulByConstantExpr
+    }
+  }
+
+  /**
+   * Holds if `expr` is effectively a division of `operand` with the
+   * positive constant `positive`.
+   */
+  private predicate dividesByPositive(DivExpr expr, Expr operand, float positive) {
+    operand = expr.(DivExpr).getLeftOperand() and
+    positive = expr.(DivExpr).getRightOperand().getValue().toFloat() and
+    positive > 0.0 // doesn't include zero
+  }
+
+  /**
+   * Holds if `expr` is effectively a division of `operand` with the
+   * negative constant `negative`.
+   */
+  private predicate dividesByNegative(Expr expr, Expr operand, float negative) {
+    operand = expr.(DivExpr).getLeftOperand() and
+    negative = getValue(expr.(DivExpr).getRightOperand().getFullyConverted()).toFloat() and
+    negative < 0.0 // doesn't include zero
+  }
+
+  /**
+   * Holds if `expr` may divide by zero. Excludes dividing a constant zero divided by zero,
+   * which produces NaN instead of an infinite value.
+   */
+  predicate dividesNonzeroByZero(Expr expr) {
+    exists(Expr divisor, Expr numerator |
+      divisor = expr.(DivExpr).getRightOperand() and
+      numerator = expr.(DivExpr).getLeftOperand() and
+      getTruncatedLowerBounds(divisor) <= 0.0 and
+      getTruncatedUpperBounds(divisor) >= 0.0 and
+      not isCheckedNotZero(divisor) and
+      not getValue(numerator).toFloat() = 0.0
+    )
+  }
+
+  bindingset[name]
+  Function getMathVariants(string name) {
+    result.hasGlobalOrStdName([name, name + "f", name + "l"])
+  }
+
+  /**
+   * New support added for mathematical functions that either monotonically increase, or decrease,
+   * or that have a known lower or upper bound.
+   *
+   * For instance, log(x) monotonically increases over x, and acos(x) monotonically decreases,
+   * while sin(x) has a known output range of -1 to 1.
+   *
+   * `pow` is especially common so minimal work is done to support that here as well. `pow(c, x)`
+   * monotonically increases or decreases over `x` if `c` is a constant, though the reverse is not
+   * true except in special cases.
+   */
+  newtype TSupportedMathFunctionCall =
+    /* A monotonically increasing function call. `extra` is a constant for `pow(x, c)`. */
+    TMonotonicIncrease(FunctionCall fc, Expr input, float extra) {
+      // Note: Codeql has no default implementation in codeql for exp2, atanh, acosh, asinh, or
+      // log1p so we haven't taken the time to support them yet.
+      fc.getTarget() =
+        getMathVariants(["log", "log2", "log10", "exp", "asin", "atan", "sinh", "sqrt"]) and
+      input = fc.getArgument(0) and
+      extra = 0.0
+      or
+      // Notes: pow is monotonic if the base argument is constant, increasing if the base is greater
+      // than 1 or between -1 and 0, and decreasing otherwise. A constant power is monotonic over the
+      // base in the positive or negative domain, but distinguishing those separately can introduce
+      // non-monotonic recursion errors.
+      fc.getTarget() = getMathVariants("pow") and
+      extra = fc.getArgument(0).getValue().toFloat() and
+      (
+        extra > 1.0
+        or
+        extra < 0.0 and extra > -1.0
+      ) and
+      input = fc.getArgument(1)
+    } or
+    /* A monotonically decreasing function call. `extra` is a constant for `pow(x, c)`. */
+    TMonotonicDecrease(FunctionCall fc, Expr input, float extra) {
+      fc.getTarget() = getMathVariants(["acos"]) and
+      input = fc.getArgument(0) and
+      extra = 0.0
+      or
+      fc.getTarget() = getMathVariants("pow") and
+      extra = fc.getArgument(0).getValue().toFloat() and
+      (
+        extra < -1.0
+        or
+        extra > 0.0 and extra < 1.0
+      ) and
+      input = fc.getArgument(1)
+    } or
+    /* A non-mononotic function call with a known lower bound. */
+    TNonMonotonicLowerBound(FunctionCall fc, float lb) {
+      fc.getTarget() = getMathVariants("cosh") and
+      lb = 1.0
+      or
+      fc.getTarget() = getMathVariants(["cos", "sin"]) and
+      lb = -1.0
+    } or
+    /* A non-mononotic function call with a known upper bound. */
+    TNonMonotonicUpperBound(FunctionCall fc, float lb) {
+      fc.getTarget() = getMathVariants(["cos", "sin"]) and
+      lb = 1.0
+    }
+
+  /**
+   * A function call that is supported by range analysis.
+   */
+  class SupportedFunctionCall extends TSupportedMathFunctionCall {
+    string toString() {
+      exists(FunctionCall fc |
+        this = TMonotonicIncrease(fc, _, _) and
+        result = "Monotonic increase " + fc.getTarget().getName()
+        or
+        this = TMonotonicDecrease(fc, _, _) and
+        result = "Monotonic decrease " + fc.getTarget().getName()
+        or
+        this = TNonMonotonicLowerBound(fc, _) and
+        result = "Nonmonotonic lower bound " + fc.getTarget().getName()
+        or
+        this = TNonMonotonicUpperBound(fc, _) and
+        result = "Nonmonotonic upper bound " + fc.getTarget().getName()
+      )
+    }
+
+    /** Get the function call node this algebraic type corresponds to. */
+    FunctionCall getFunctionCall() {
+      this = TMonotonicIncrease(result, _, _)
+      or
+      this = TMonotonicDecrease(result, _, _)
+      or
+      this = TNonMonotonicLowerBound(result, _)
+      or
+      this = TNonMonotonicUpperBound(result, _)
+    }
+
+    /** Get the function name (`sin`, `pow`, etc.) without the `l` or `f` suffix. */
+    bindingset[this, result]
+    string getBaseFunctionName() { getMathVariants(result) = getFunctionCall().getTarget() }
+
+    /**
+     * Compute a result bound based on an input value and an extra constant value.
+     *
+     * The functions `getUpperBound()` and `getLowerBound()` automatically handle the differences
+     * between monotonically increasing and decreasing functions, and provide the input value. The
+     * `extra` float exists to support `pow(x, c)` for the constant `c`, otherwise it is `0.0`.
+     */
+    bindingset[value, extra, this]
+    float compute(float value, float extra) {
+      exists(string name | name = getBaseFunctionName() |
+        name = "log" and
+        result = value.log()
+        or
+        name = "log2" and
+        result = value.log2()
+        or
+        name = "log10" and
+        result = value.log10()
+        or
+        name = "exp" and
+        result = value.exp()
+        or
+        name = "asin" and
+        result = value.asin()
+        or
+        name = "atan" and
+        result = value.atan()
+        or
+        name = "acos" and
+        result = value.acos()
+        or
+        name = "sinh" and
+        result = value.sinh()
+        or
+        name = "sqrt" and
+        result = value.sqrt()
+        or
+        name = "pow" and
+        result = extra.pow(value)
+      )
+    }
+
+    /**
+     * Get the lower bound of this function, based on its fixed range (if it has one) or based on
+     * the lower or upper bound of its input, if it is a monotonically increasing or decreasing
+     * function.
+     */
+    float getLowerBound() {
+      this = TNonMonotonicLowerBound(_, result)
+      or
+      exists(Expr expr, float bound, float extra |
+        (
+          this = TMonotonicIncrease(_, expr, extra) and
+          bound = getFullyConvertedLowerBounds(expr)
+          or
+          this = TMonotonicDecrease(_, expr, extra) and
+          bound = getFullyConvertedUpperBounds(expr)
+        ) and
+        result = compute(bound, extra)
+      )
+    }
+
+    /**
+     * Get the lower bound of this function, based on its fixed range (if it has one) or based on
+     * the lower or upper bound of its input, if it is a monotonically increasing or decreasing
+     * function.
+     */
+    float getUpperBound() {
+      this = TNonMonotonicUpperBound(_, result)
+      or
+      exists(Expr expr, float bound, float extra |
+        (
+          this = TMonotonicIncrease(_, expr, extra) and
+          bound = getFullyConvertedUpperBounds(expr)
+          or
+          this = TMonotonicDecrease(_, expr, extra) and
+          bound = getFullyConvertedLowerBounds(expr)
+        ) and
+        result = compute(bound, extra)
+      )
+    }
+  }
+
+  predicate supportedMathFunction(FunctionCall fc) {
+    exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = fc)
+  }
+
+  /**
+   * Holds if `expr` is checked with a guard to not be zero.
+   *
+   * Since our range analysis only tracks an upper and lower bound, that means if a variable has
+   * range [-10, 10], its range includes zero. In the body of an if statement that checks it's not
+   * equal to zero, we cannot update the range to reflect that as the upper and lower bounds are
+   * not changed. This problem is not the case for gt, lt, gte, lte, or ==, as these can be used to
+   * create a new subset range that does not include zero.
+   *
+   * It is important to know if an expr may be zero to avoid division by zero creating infinities.
+   */
+  predicate isCheckedNotZero(Expr expr) {
+    exists(RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard |
+      // This is copied from getGuardedUpperBound, which says its only an approximation. This is
+      // indeed wrong in many cases.
+      def.isGuardPhi(v, guardVa, guard, _) and
+      exists(unique(BasicBlock b | b = def.(BasicBlock).getAPredecessor())) and
+      expr = def.getAUse(v) and
+      isNEPhi(v, def, guardVa, 0)
+    )
+    or
+    guardedHashConsNotEqualZero(expr)
+  }
+
+  predicate guardedHashConsNotEqualZero(Expr e) {
+    /* Note Boolean cmpEq, false means cmpNeq */
+    exists(Expr check, Expr val, int valVal, GuardCondition guard, boolean cmpEq |
+      hashCons(check) = hashCons(e) and
+      valVal = getValue(val).toFloat() and
+      guard.controls(e.getBasicBlock(), cmpEq) and
+      (
+        guard.comparesEq(check, val, -valVal, false, cmpEq) or
+        guard.comparesEq(val, check, -valVal, false, cmpEq)
+      )
+    )
+  }
+
+  /** Set of expressions which we know how to analyze. */
+  predicate analyzableExpr(Expr e) {
+    // The type of the expression must be arithmetic. We reuse the logic in
+    // `exprMinVal` to check this.
+    exists(Util::exprMinVal(e)) and
+    (
+      exists(getValue(e).toFloat())
+      or
+      effectivelyMultipliesByPositive(e, _, _)
+      or
+      effectivelyMultipliesByNegative(e, _, _)
+      or
+      dividesByPositive(e, _, _)
+      or
+      dividesByNegative(e, _, _)
+      or
+      // Introduces non-monotonic recursion. However, analysis mostly works with this
+      // commented out.
+      // or
+      // dividesNonzeroByZero(e)
+      e instanceof DivExpr // TODO: confirm this is OK
+      or
+      supportedMathFunction(e)
+      or
+      e instanceof MinExpr
+      or
+      e instanceof MaxExpr
+      or
+      e instanceof ConditionalExpr
+      or
+      e instanceof AddExpr
+      or
+      e instanceof SubExpr
+      or
+      e instanceof UnsignedMulExpr
+      or
+      e instanceof AssignExpr
+      or
+      e instanceof AssignAddExpr
+      or
+      e instanceof AssignSubExpr
+      or
+      e instanceof UnsignedAssignMulExpr
+      or
+      e instanceof AssignMulByConstantExpr
+      or
+      e instanceof CrementOperation
+      or
+      e instanceof RemExpr
+      or
+      // A conversion is analyzable, provided that its child has an arithmetic
+      // type. (Sometimes the child is a reference type, and so does not get
+      // any bounds.) Rather than checking whether the type of the child is
+      // arithmetic, we reuse the logic that is already encoded in
+      // `exprMinVal`.
+      exists(Util::exprMinVal(e.(Conversion).getExpr()))
+      or
+      // Also allow variable accesses, provided that they have SSA
+      // information.
+      exists(RangeSsaDefinition def | e = def.getAUse(_))
+      or
+      e instanceof UnsignedBitwiseAndExpr
+      or
+      // `>>` by a constant
+      exists(getValue(e.(RShiftExpr).getRightOperand()))
+    )
+  }
+
+  /**
+   * Set of definitions that this definition depends on. The transitive
+   * closure of this relation is used to detect definitions which are
+   * recursively defined, so that we can prevent the analysis from exploding.
+   *
+   * The structure of `defDependsOnDef` and its helper predicates matches the
+   * structure of `getDefLowerBoundsImpl` and
+   * `getDefUpperBoundsImpl`. Therefore, if changes are made to the structure
+   * of the main analysis algorithm then matching changes need to be made
+   * here.
+   */
+  private predicate defDependsOnDef(
+    RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
+  ) {
+    // Definitions with a defining value.
+    exists(Expr expr | assignmentDef(def, v, expr) | exprDependsOnDef(expr, srcDef, srcVar))
+    or
+    // Assignment operations with a defining value
+    exists(AssignOperation assignOp |
+      analyzableExpr(assignOp) and
+      def = assignOp and
+      def.getAVariable() = v and
+      exprDependsOnDef(assignOp, srcDef, srcVar)
+    )
+    or
+    exists(CrementOperation crem |
+      def = crem and
+      def.getAVariable() = v and
+      exprDependsOnDef(crem.getOperand(), srcDef, srcVar)
+    )
+    or
+    // Phi nodes.
+    phiDependsOnDef(def, v, srcDef, srcVar)
+  }
+
+  /**
+   * Helper predicate for `defDependsOnDef`. This predicate matches
+   * the structure of `getLowerBoundsImpl` and `getUpperBoundsImpl`.
+   */
+  private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVariable srcVar) {
+    exists(Expr operand |
+      effectivelyMultipliesByNegative(e, operand, _) and
+      exprDependsOnDef(operand, srcDef, srcVar)
+    )
+    or
+    exists(Expr operand |
+      effectivelyMultipliesByPositive(e, operand, _) and
+      exprDependsOnDef(operand, srcDef, srcVar)
+    )
+    or
+    exists(Expr operand |
+      (dividesByPositive(e, operand, _) or dividesByNegative(e, operand, _)) and
+      exprDependsOnDef(operand, srcDef, srcVar)
+    )
+    or
+    exists(DivExpr div | div = e | exprDependsOnDef(div.getAnOperand(), srcDef, srcVar))
+    or
+    exists(MinExpr minExpr | e = minExpr | exprDependsOnDef(minExpr.getAnOperand(), srcDef, srcVar))
+    or
+    exists(MaxExpr maxExpr | e = maxExpr | exprDependsOnDef(maxExpr.getAnOperand(), srcDef, srcVar))
+    or
+    exists(ConditionalExpr condExpr | e = condExpr |
+      exprDependsOnDef(condExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    exists(AddExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar))
+    or
+    exists(SubExpr subExpr | e = subExpr | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
+    or
+    exists(UnsignedMulExpr mulExpr | e = mulExpr |
+      exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    exists(AssignExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getRValue(), srcDef, srcVar))
+    or
+    exists(AssignAddExpr addExpr | e = addExpr |
+      exprDependsOnDef(addExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    exists(AssignSubExpr subExpr | e = subExpr |
+      exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    exists(UnsignedAssignMulExpr mulExpr | e = mulExpr |
+      exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    exists(AssignMulByConstantExpr mulExpr | e = mulExpr |
+      exprDependsOnDef(mulExpr.getLValue(), srcDef, srcVar)
+    )
+    or
+    exists(CrementOperation crementExpr | e = crementExpr |
+      exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar)
+    )
+    or
+    exists(RemExpr remExpr | e = remExpr | exprDependsOnDef(remExpr.getAnOperand(), srcDef, srcVar))
+    or
+    exists(Conversion convExpr | e = convExpr |
+      exprDependsOnDef(convExpr.getExpr(), srcDef, srcVar)
+    )
+    or
+    // unsigned `&`
+    exists(UnsignedBitwiseAndExpr andExpr |
+      andExpr = e and
+      exprDependsOnDef(andExpr.getAnOperand(), srcDef, srcVar)
+    )
+    or
+    // `>>` by a constant
+    exists(RShiftExpr rs |
+      rs = e and
+      exists(getValue(rs.getRightOperand())) and
+      exprDependsOnDef(rs.getLeftOperand(), srcDef, srcVar)
+    )
+    or
+    e = srcDef.getAUse(srcVar)
+  }
+
+  /**
+   * Helper predicate for `defDependsOnDef`. This predicate matches
+   * the structure of `getPhiLowerBounds` and `getPhiUpperBounds`.
+   */
+  private predicate phiDependsOnDef(
+    RangeSsaDefinition phi, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
+  ) {
+    exists(VariableAccess access, Expr guard | phi.isGuardPhi(v, access, guard, _) |
+      exprDependsOnDef(guard.(ComparisonOperation).getAnOperand(), srcDef, srcVar) or
+      exprDependsOnDef(access, srcDef, srcVar)
+    )
+    or
+    srcDef = phi.getAPhiInput(v) and srcVar = v
+  }
+
+  /** The transitive closure of `defDependsOnDef`. */
+  private predicate defDependsOnDefTransitively(
+    RangeSsaDefinition def, StackVariable v, RangeSsaDefinition srcDef, StackVariable srcVar
+  ) {
+    defDependsOnDef(def, v, srcDef, srcVar)
+    or
+    exists(RangeSsaDefinition midDef, StackVariable midVar |
+      defDependsOnDef(def, v, midDef, midVar)
+    |
+      defDependsOnDefTransitively(midDef, midVar, srcDef, srcVar)
+    )
+  }
+
+  /** The set of definitions that depend recursively on themselves. */
+  private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) {
+    defDependsOnDefTransitively(def, v, def, v)
+  }
+
+  /**
+   * Holds if the bounds of `e` depend on a recursive definition, meaning that
+   * `e` is likely to have many candidate bounds during the main recursion.
+   */
+  private predicate isRecursiveExpr(Expr e) {
+    exists(RangeSsaDefinition def, StackVariable v | exprDependsOnDef(e, def, v) |
+      isRecursiveDef(def, v)
+    )
+  }
+
+  /**
+   * Holds if `binop` is a binary operation that's likely to be assigned a
+   * quadratic (or more) number of candidate bounds during the analysis. This can
+   * happen when two conditions are satisfied:
+   * 1. It is likely there are many more candidate bounds for `binop` than for
+   *    its operands. For example, the number of candidate bounds for `x + y`,
+   *    denoted here nbounds(`x + y`), will be O(nbounds(`x`) * nbounds(`y`)).
+   *    In contrast, nbounds(`b ? x : y`) is only O(nbounds(`x`) + nbounds(`y`)).
+   * 2. Both operands of `binop` are recursively determined and are therefore
+   *    likely to have a large number of candidate bounds.
+   */
+  private predicate isRecursiveBinary(BinaryOperation binop) {
+    (
+      binop instanceof UnsignedMulExpr
+      or
+      binop instanceof AddExpr
+      or
+      binop instanceof SubExpr
+    ) and
+    isRecursiveExpr(binop.getLeftOperand()) and
+    isRecursiveExpr(binop.getRightOperand())
+  }
+
+  private predicate applyWideningToBinary(BinaryOperation op) {
+    // Original behavior:
+    isRecursiveBinary(op)
+    or
+    // As we added support for DivExpr, we found cases of combinatorial explosion that are not
+    // caused by recursion. Given expr `x` that depends on a phi node that has evaluated y unique
+    // values, `x + x` will in the worst case evaluate to y^2 unique values, even if `x` is not
+    // recursive. By adding support for division, we have revealed certain pathological cases in
+    // open source code, for instance `posix_time_from_utc` from boringssl. We can reduce this
+    // greatly by widening, and targeting division effectively reduces the chains of evaluations
+    // that cause this issue while preserving the original behavior.
+    //
+    // There is also a set of functions intended to estimate the combinations of phi nodes each
+    // expression depends on, which could be used to accurately widen only expensive nodes. However,
+    // that estimation is more involved than it may seem, and hasn't yet resulted in a net
+    // improvement. See `estimatedPhiCombinationsExpr` and `estimatedPhiCombinationsDef`.
+    //
+    // This approach currently has the best performance.
+    op instanceof DivExpr
+  }
+
+  /**
+   * Recursively scan this expr to see how many phi nodes it depends on. Binary expressions
+   * induce a combination effect, so `a + b` where `a` depends on 3 phi nodes and `b` depends on 4
+   * will induce 3*4 = 12 phi node combinations.
+   *
+   * This currently requires additional optimization to be useful in practice.
+   */
+  int estimatedPhiCombinationsExpr(Expr expr) {
+    if isRecursiveExpr(expr)
+    then
+      // Assume 10 values were computed to analyze recursive expressions.
+      result = 10
+    else (
+      exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) |
+        def.isPhiNode(v) and
+        result = estimatedPhiCombinationsDef(def, v)
+      )
+      or
+      exists(BinaryOperation binop |
+        binop = expr and
+        result =
+          estimatedPhiCombinationsExpr(binop.getLeftOperand()) *
+            estimatedPhiCombinationsExpr(binop.getRightOperand())
+      )
+      or
+      not expr instanceof BinaryOperation and
+      exists(RangeSsaDefinition def, StackVariable v | exprDependsOnDef(expr, def, v) |
+        result = estimatedPhiCombinationsDef(def, v)
+      )
+      or
+      not expr instanceof BinaryOperation and
+      not exprDependsOnDef(expr, _, _) and
+      result = 1
+    )
+  }
+
+  /**
+   * Recursively scan this def to see how many phi nodes it depends on.
+   *
+   * If this def is a phi node, it sums its downstream cost and adds one to account for itself,
+   * which is not exactly correct.
+   *
+   * This def may also be a crement expression (not currently supported), or an assign expr
+   * (currently not supported), or an unanalyzable expression which is the root of the recursion
+   * and given a value of 1.
+   */
+  language[monotonicAggregates]
+  int estimatedPhiCombinationsDef(RangeSsaDefinition def, StackVariable v) {
+    if isRecursiveDef(def, v)
+    then
+      // Assume 10 values were computed to analyze recursive expressions.
+      result = 10
+    else (
+      if def.isPhiNode(v)
+      then
+        exists(Expr e | e = def.getAUse(v) |
+          result =
+            1 +
+              sum(RangeSsaDefinition srcDef |
+                srcDef = def.getAPhiInput(v)
+              |
+                estimatedPhiCombinationsDef(srcDef, v)
+              )
+        )
+      else (
+        exists(Expr expr | assignmentDef(def, v, expr) |
+          result = estimatedPhiCombinationsExpr(expr)
+        )
+        or
+        v = def.getAVariable() and
+        not assignmentDef(def, v, _) and
+        result = 1
+      )
+    )
+  }
+
+  /**
+   * We distinguish 3 kinds of RangeSsaDefinition:
+   *
+   * 1. Definitions with a defining value.
+   *    For example: x = y+3 is a definition of x with defining value y+3.
+   *
+   * 2. Phi nodes: x3 = phi(x0,x1,x2)
+   *
+   * 3. Unanalyzable definitions.
+   *    For example: a parameter is unanalyzable because we know nothing
+   *    about its value. We assign these range [-largeValue(), largeValue()]
+   *
+   * This predicate finds all the definitions in the first set.
+   */
+  private predicate assignmentDef(RangeSsaDefinition def, StackVariable v, Expr expr) {
+    Util::getVariableRangeType(v) instanceof ArithmeticType and
+    (
+      def = v.getInitializer().getExpr() and def = expr
+      or
+      exists(AssignExpr assign |
+        def = assign and
+        assign.getLValue() = v.getAnAccess() and
+        expr = assign.getRValue()
+      )
+    )
+  }
+
+  /** See comment above assignmentDef. */
+  private predicate analyzableDef(RangeSsaDefinition def, StackVariable v) {
+    assignmentDef(def, v, _)
+    or
+    analyzableExpr(def.(AssignOperation)) and
+    v = def.getAVariable()
+    or
+    analyzableExpr(def.(CrementOperation)) and
+    v = def.getAVariable()
+    or
+    phiDependsOnDef(def, v, _, _)
+  }
+
+  predicate canBoundExpr(Expr e) {
+    exists(RangeSsaDefinition def, StackVariable v | e = def.getAUse(v) | analyzableDef(def, v))
+    or
+    analyzableExpr(e)
+    or
+    exists(getGuardedUpperBound(e))
+    or
+    lowerBoundFromGuard(e, _, _, _)
+  }
+
+  /**
+   * 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) or dividesNonzeroByZero(expr)) and
+    getUpperBoundsImpl(expr) <= Util::exprMaxVal(expr) and
+    not exists(getValue(expr).toFloat())
+  }
+
+  /**
+   * Gets the lower bounds of the expression.
+   *
+   * Most of the work of computing the lower bounds is done by
+   * `getLowerBoundsImpl`. However, the lower bounds computed by
+   * `getLowerBoundsImpl` may not be representable by the result type of the
+   * expression. For example, if `x` and `y` are of type `int32` and each
+   * have lower bound -2147483648, then getLowerBoundsImpl` will compute a
+   * lower bound -4294967296 for the expression `x+y`, even though
+   * -4294967296 cannot be represented as an `int32`. Such unrepresentable
+   * bounds are replaced with `exprMinVal(expr)`. This predicate also adds
+   * `exprMinVal(expr)` as a lower bound if the expression might overflow
+   * positively, or if it is unanalyzable.
+   *
+   * Note: most callers should use `getFullyConvertedLowerBounds` rather than
+   * this predicate.
+   */
+  private float 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()
+    or
+    // Some of the bounds computed by getLowerBoundsImpl might
+    // overflow, so we replace invalid bounds with exprMinVal.
+    exists(float newLB | newLB = normalizeFloatUp(getLowerBoundsImpl(expr)) |
+      if Util::exprMinVal(expr) <= newLB and newLB <= Util::exprMaxVal(expr)
+      then
+        // Apply widening where we might get a combinatorial explosion.
+        if applyWideningToBinary(expr)
+        then
+          result =
+            max(float widenLB |
+              widenLB = wideningLowerBounds(expr.getUnspecifiedType()) and
+              not widenLB > newLB
+            )
+        else result = newLB
+      else result = Util::exprMinVal(expr)
+    ) and
+    lowerBoundableExpr(expr)
+    or
+    // The expression might overflow and wrap. If so, the
+    // lower bound is exprMinVal.
+    analyzableExpr(expr) and
+    exprMightOverflowPositively(expr) and
+    not result = getValue(expr).toFloat() and
+    result = Util::exprMinVal(expr)
+    or
+    // The expression is not analyzable, so its lower bound is
+    // unknown. Note that the call to exprMinVal restricts the
+    // expressions to just those with arithmetic types. There is no
+    // need to return results for non-arithmetic expressions.
+    not analyzableExpr(expr) and
+    result = exprMinVal(expr)
+  }
+
+  /**
+   * Gets the upper bounds of the expression.
+   *
+   * Most of the work of computing the upper bounds is done by
+   * `getUpperBoundsImpl`. However, the upper bounds computed by
+   * `getUpperBoundsImpl` may not be representable by the result type of the
+   * expression. For example, if `x` and `y` are of type `int32` and each
+   * have upper bound 2147483647, then getUpperBoundsImpl` will compute an
+   * upper bound 4294967294 for the expression `x+y`, even though 4294967294
+   * cannot be represented as an `int32`. Such unrepresentable bounds are
+   * replaced with `exprMaxVal(expr)`.  This predicate also adds
+   * `exprMaxVal(expr)` as an upper bound if the expression might overflow
+   * negatively, or if it is unanalyzable.
+   *
+   * Note: most callers should use `getFullyConvertedUpperBounds` rather than
+   * this predicate.
+   */
+  private float getTruncatedUpperBounds(Expr expr) {
+    (analyzableExpr(expr) or dividesNonzeroByZero(expr)) and
+    (
+      // 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()
+      else (
+        // Some of the bounds computed by `getUpperBoundsImpl`
+        // might overflow, so we replace invalid bounds with
+        // `exprMaxVal`.
+        exists(float newUB | newUB = normalizeFloatUp(getUpperBoundsImpl(expr)) |
+          if Util::exprMinVal(expr) <= newUB and newUB <= Util::exprMaxVal(expr)
+          then
+            // Apply widening where we might get a combinatorial explosion.
+            if applyWideningToBinary(expr)
+            then
+              result =
+                min(float widenUB |
+                  widenUB = wideningUpperBounds(expr.getUnspecifiedType()) and
+                  not widenUB < newUB
+                )
+            else result = newUB
+          else result = Util::exprMaxVal(expr)
+        )
+        or
+        // The expression might overflow negatively and wrap. If so,
+        // the upper bound is `exprMaxVal`.
+        exprMightOverflowNegatively(expr) and
+        result = Util::exprMaxVal(expr)
+      )
+    )
+    or
+    not analyzableExpr(expr) and
+    // The expression is not analyzable, so its upper bound is
+    // unknown. Note that the call to exprMaxVal restricts the
+    // expressions to just those with arithmetic types. There is no
+    // need to return results for non-arithmetic expressions.
+    result = exprMaxVal(expr)
+  }
+
+  /** Only to be called by `getTruncatedLowerBounds`. */
+  private float getLowerBoundsImpl(Expr expr) {
+    (
+      exists(Expr operand, float operandLow, float positive |
+        effectivelyMultipliesByPositive(expr, operand, positive) and
+        operandLow = getFullyConvertedLowerBounds(operand) and
+        result = positive * operandLow
+      )
+      or
+      exists(Expr operand, float operandHigh, float negative |
+        effectivelyMultipliesByNegative(expr, operand, negative) and
+        operandHigh = getFullyConvertedUpperBounds(operand) and
+        result = negative * operandHigh
+      )
+      or
+      exists(Expr operand, float operandLow, float positive |
+        dividesByPositive(expr, operand, positive) and
+        operandLow = getFullyConvertedLowerBounds(operand) and
+        result = operandLow / positive
+      )
+      or
+      exists(Expr operand, float operandLow, float negative |
+        dividesByNegative(expr, operand, negative) and
+        operandLow = getFullyConvertedUpperBounds(operand) and
+        result = operandLow / negative
+      )
+      or
+      exists(DivExpr div | expr = div |
+        dividesNonzeroByZero(expr) and
+        result = getFullyConvertedLowerBounds(div.getLeftOperand()) / 0
+      )
+      or
+      exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = expr |
+        result = sfc.getLowerBound()
+      )
+      or
+      exists(MinExpr minExpr |
+        expr = minExpr and
+        // Return the union of the lower bounds from both children.
+        result = getFullyConvertedLowerBounds(minExpr.getAnOperand())
+      )
+      or
+      exists(MaxExpr maxExpr |
+        expr = maxExpr and
+        // Compute the cross product of the bounds from both children.  We are
+        // using this mathematical property:
+        //
+        //    max (minimum{X}, minimum{Y})
+        //  = minimum { max(x,y) | x in X, y in Y }
+        exists(float x, float y |
+          x = getFullyConvertedLowerBounds(maxExpr.getLeftOperand()) and
+          y = getFullyConvertedLowerBounds(maxExpr.getRightOperand()) and
+          if x >= y then result = x else result = y
+        )
+      )
+      or
+      // ConditionalExpr (true branch)
+      exists(ConditionalExpr condExpr |
+        expr = condExpr and
+        // Use `boolConversionUpperBound` to determine whether the condition
+        // might evaluate to `true`.
+        boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
+        result = getFullyConvertedLowerBounds(condExpr.getThen())
+      )
+      or
+      // ConditionalExpr (false branch)
+      exists(ConditionalExpr condExpr |
+        expr = condExpr and
+        // Use `boolConversionLowerBound` to determine whether the condition
+        // might evaluate to `false`.
+        boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
+        result = getFullyConvertedLowerBounds(condExpr.getElse())
+      )
+      or
+      exists(AddExpr addExpr, float xLow, float yLow |
+        expr = addExpr and
+        xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and
+        yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and
+        result = addRoundingDown(xLow, yLow)
+      )
+      or
+      exists(SubExpr subExpr, float xLow, float yHigh |
+        expr = subExpr and
+        xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and
+        yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
+        result = addRoundingDown(xLow, -yHigh)
+      )
+      or
+      exists(UnsignedMulExpr mulExpr, float xLow, float yLow |
+        expr = mulExpr and
+        xLow = getFullyConvertedLowerBounds(mulExpr.getLeftOperand()) and
+        yLow = getFullyConvertedLowerBounds(mulExpr.getRightOperand()) and
+        result = xLow * yLow
+      )
+      or
+      exists(AssignExpr assign |
+        expr = assign and
+        result = getFullyConvertedLowerBounds(assign.getRValue())
+      )
+      or
+      exists(AssignAddExpr addExpr, float xLow, float yLow |
+        expr = addExpr and
+        xLow = getFullyConvertedLowerBounds(addExpr.getLValue()) and
+        yLow = getFullyConvertedLowerBounds(addExpr.getRValue()) and
+        result = addRoundingDown(xLow, yLow)
+      )
+      or
+      exists(AssignSubExpr subExpr, float xLow, float yHigh |
+        expr = subExpr and
+        xLow = getFullyConvertedLowerBounds(subExpr.getLValue()) and
+        yHigh = getFullyConvertedUpperBounds(subExpr.getRValue()) and
+        result = addRoundingDown(xLow, -yHigh)
+      )
+      or
+      exists(UnsignedAssignMulExpr mulExpr, float xLow, float yLow |
+        expr = mulExpr and
+        xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
+        yLow = getFullyConvertedLowerBounds(mulExpr.getRValue()) and
+        result = xLow * yLow
+      )
+      or
+      exists(AssignMulByPositiveConstantExpr mulExpr, float xLow |
+        expr = mulExpr and
+        xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
+        result = xLow * mulExpr.getConstant()
+      )
+      or
+      exists(AssignMulByNegativeConstantExpr mulExpr, float xHigh |
+        expr = mulExpr and
+        xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
+        result = xHigh * mulExpr.getConstant()
+      )
+      or
+      exists(PrefixIncrExpr incrExpr, float xLow |
+        expr = incrExpr and
+        xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
+        result = xLow + 1
+      )
+      or
+      exists(PrefixDecrExpr decrExpr, float xLow |
+        expr = decrExpr and
+        xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and
+        result = addRoundingDownSmall(xLow, -1)
+      )
+      or
+      // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their
+      // operand. The incrementing/decrementing behavior is handled in
+      // `getDefLowerBoundsImpl`.
+      exists(PostfixIncrExpr incrExpr |
+        expr = incrExpr and
+        result = getFullyConvertedLowerBounds(incrExpr.getOperand())
+      )
+      or
+      exists(PostfixDecrExpr decrExpr |
+        expr = decrExpr and
+        result = getFullyConvertedLowerBounds(decrExpr.getOperand())
+      )
+      or
+      exists(RemExpr remExpr | expr = remExpr |
+        // If both inputs are positive then the lower bound is zero.
+        result = 0
+        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 |
+          childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
+          not childLB >= 0
+        |
+          result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
+          or
+          exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) |
+            result = -rhsUB + 1
+          )
+        )
+      )
+      or
+      // If the conversion is to an arithmetic type then we just return the
+      // lower bound of the child. We do not need to handle truncation and
+      // overflow here, because that is done in `getTruncatedLowerBounds`.
+      // Conversions to `bool` need to be handled specially because they test
+      // whether the value of the expression is equal to 0.
+      exists(Conversion convExpr | expr = convExpr |
+        if convExpr.getUnspecifiedType() instanceof BoolType
+        then result = boolConversionLowerBound(convExpr.getExpr())
+        else result = getTruncatedLowerBounds(convExpr.getExpr())
+      )
+      or
+      // Use SSA to get the lower bounds for a variable use.
+      exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) |
+        result = getDefLowerBounds(def, v)
+      )
+      or
+      // unsigned `&` (tighter bounds may exist)
+      exists(UnsignedBitwiseAndExpr andExpr |
+        andExpr = expr and
+        result = 0.0
+      )
+      or
+      // `>>` by a constant
+      exists(RShiftExpr rsExpr, float left, int right |
+        rsExpr = expr and
+        left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and
+        right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
+        result = safeFloor(left / 2.pow(right))
+      )
+    )
+  }
+
+  /** Only to be called by `getTruncatedUpperBounds`. */
+  private float getUpperBoundsImpl(Expr expr) {
+    (
+      exists(Expr operand, float operandHigh, float positive |
+        effectivelyMultipliesByPositive(expr, operand, positive) and
+        operandHigh = getFullyConvertedUpperBounds(operand) and
+        result = positive * operandHigh
+      )
+      or
+      exists(Expr operand, float operandLow, float negative |
+        effectivelyMultipliesByNegative(expr, operand, negative) and
+        operandLow = getFullyConvertedLowerBounds(operand) and
+        result = negative * operandLow
+      )
+      or
+      exists(Expr operand, float operandHigh, float positive |
+        dividesByPositive(expr, operand, positive) and
+        operandHigh = getFullyConvertedUpperBounds(operand) and
+        result = operandHigh / positive
+      )
+      or
+      exists(Expr operand, float operandHigh, float negative |
+        dividesByNegative(expr, operand, negative) and
+        operandHigh = getFullyConvertedLowerBounds(operand) and
+        result = operandHigh / negative
+      )
+      or
+      exists(DivExpr div | expr = div |
+        dividesNonzeroByZero(expr) and
+        result = getFullyConvertedUpperBounds(div.getLeftOperand()) / 0
+      )
+      or
+      exists(SupportedFunctionCall sfc | sfc.getFunctionCall() = expr |
+        result = sfc.getUpperBound()
+      )
+      or
+      exists(MaxExpr maxExpr |
+        expr = maxExpr and
+        // Return the union of the upper bounds from both children.
+        result = getFullyConvertedUpperBounds(maxExpr.getAnOperand())
+      )
+      or
+      exists(MinExpr minExpr |
+        expr = minExpr and
+        // Compute the cross product of the bounds from both children.  We are
+        // using this mathematical property:
+        //
+        //    min (maximum{X}, maximum{Y})
+        //  = maximum { min(x,y) | x in X, y in Y }
+        exists(float x, float y |
+          x = getFullyConvertedUpperBounds(minExpr.getLeftOperand()) and
+          y = getFullyConvertedUpperBounds(minExpr.getRightOperand()) and
+          if x <= y then result = x else result = y
+        )
+      )
+      or
+      // ConditionalExpr (true branch)
+      exists(ConditionalExpr condExpr |
+        expr = condExpr and
+        // Use `boolConversionUpperBound` to determine whether the condition
+        // might evaluate to `true`.
+        boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
+        result = getFullyConvertedUpperBounds(condExpr.getThen())
+      )
+      or
+      // ConditionalExpr (false branch)
+      exists(ConditionalExpr condExpr |
+        expr = condExpr and
+        // Use `boolConversionLowerBound` to determine whether the condition
+        // might evaluate to `false`.
+        boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
+        result = getFullyConvertedUpperBounds(condExpr.getElse())
+      )
+      or
+      exists(AddExpr addExpr, float xHigh, float yHigh |
+        expr = addExpr and
+        xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and
+        yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and
+        result = addRoundingUp(xHigh, yHigh)
+      )
+      or
+      exists(SubExpr subExpr, float xHigh, float yLow |
+        expr = subExpr and
+        xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and
+        yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
+        result = addRoundingUp(xHigh, -yLow)
+      )
+      or
+      exists(UnsignedMulExpr mulExpr, float xHigh, float yHigh |
+        expr = mulExpr and
+        xHigh = getFullyConvertedUpperBounds(mulExpr.getLeftOperand()) and
+        yHigh = getFullyConvertedUpperBounds(mulExpr.getRightOperand()) and
+        result = xHigh * yHigh
+      )
+      or
+      exists(AssignExpr assign |
+        expr = assign and
+        result = getFullyConvertedUpperBounds(assign.getRValue())
+      )
+      or
+      exists(AssignAddExpr addExpr, float xHigh, float yHigh |
+        expr = addExpr and
+        xHigh = getFullyConvertedUpperBounds(addExpr.getLValue()) and
+        yHigh = getFullyConvertedUpperBounds(addExpr.getRValue()) and
+        result = addRoundingUp(xHigh, yHigh)
+      )
+      or
+      exists(AssignSubExpr subExpr, float xHigh, float yLow |
+        expr = subExpr and
+        xHigh = getFullyConvertedUpperBounds(subExpr.getLValue()) and
+        yLow = getFullyConvertedLowerBounds(subExpr.getRValue()) and
+        result = addRoundingUp(xHigh, -yLow)
+      )
+      or
+      exists(UnsignedAssignMulExpr mulExpr, float xHigh, float yHigh |
+        expr = mulExpr and
+        xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
+        yHigh = getFullyConvertedUpperBounds(mulExpr.getRValue()) and
+        result = xHigh * yHigh
+      )
+      or
+      exists(AssignMulByPositiveConstantExpr mulExpr, float xHigh |
+        expr = mulExpr and
+        xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
+        result = xHigh * mulExpr.getConstant()
+      )
+      or
+      exists(AssignMulByNegativeConstantExpr mulExpr, float xLow |
+        expr = mulExpr and
+        xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
+        result = xLow * mulExpr.getConstant()
+      )
+      or
+      exists(PrefixIncrExpr incrExpr, float xHigh |
+        expr = incrExpr and
+        xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
+        result = addRoundingUpSmall(xHigh, 1)
+      )
+      or
+      exists(PrefixDecrExpr decrExpr, float xHigh |
+        expr = decrExpr and
+        xHigh = getFullyConvertedUpperBounds(decrExpr.getOperand()) and
+        result = xHigh - 1
+      )
+      or
+      // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their operand.
+      // The incrementing/decrementing behavior is handled in
+      // `getDefUpperBoundsImpl`.
+      exists(PostfixIncrExpr incrExpr |
+        expr = incrExpr and
+        result = getFullyConvertedUpperBounds(incrExpr.getOperand())
+      )
+      or
+      exists(PostfixDecrExpr decrExpr |
+        expr = decrExpr and
+        result = getFullyConvertedUpperBounds(decrExpr.getOperand())
+      )
+      or
+      exists(RemExpr remExpr, float rhsUB |
+        expr = remExpr and
+        rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
+      |
+        result = rhsUB - 1
+        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 |
+          rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
+          not rhsLB >= 0
+        |
+          result = -rhsLB + 1
+        )
+      )
+      or
+      // If the conversion is to an arithmetic type then we just return the
+      // upper bound of the child. We do not need to handle truncation and
+      // overflow here, because that is done in `getTruncatedUpperBounds`.
+      // Conversions to `bool` need to be handled specially because they test
+      // whether the value of the expression is equal to 0.
+      exists(Conversion convExpr | expr = convExpr |
+        if convExpr.getUnspecifiedType() instanceof BoolType
+        then result = boolConversionUpperBound(convExpr.getExpr())
+        else result = getTruncatedUpperBounds(convExpr.getExpr())
+      )
+      or
+      // Use SSA to get the upper bounds for a variable use.
+      exists(RangeSsaDefinition def, StackVariable v | expr = def.getAUse(v) |
+        result = getDefUpperBounds(def, v)
+      )
+      or
+      // unsigned `&` (tighter bounds may exist)
+      exists(UnsignedBitwiseAndExpr andExpr, float left, float right |
+        andExpr = expr and
+        left = getFullyConvertedUpperBounds(andExpr.getLeftOperand()) and
+        right = getFullyConvertedUpperBounds(andExpr.getRightOperand()) and
+        result = left.minimum(right)
+      )
+      or
+      // `>>` by a constant
+      exists(RShiftExpr rsExpr, float left, int right |
+        rsExpr = expr and
+        left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and
+        right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
+        result = safeFloor(left / 2.pow(right))
+      )
+    )
+  }
+
+  /**
+   * Holds if `expr` is converted to `bool` or if it is the child of a
+   * logical operation.
+   *
+   * The purpose of this predicate is to optimize `boolConversionLowerBound`
+   * and `boolConversionUpperBound` by preventing them from computing
+   * unnecessary results. In other words, `exprIsUsedAsBool(expr)` holds if
+   * `expr` is an expression that might be passed as an argument to
+   * `boolConversionLowerBound` or `boolConversionUpperBound`.
+   */
+  private predicate exprIsUsedAsBool(Expr expr) {
+    expr = any(BinaryLogicalOperation op).getAnOperand().getFullyConverted()
+    or
+    expr = any(UnaryLogicalOperation op).getOperand().getFullyConverted()
+    or
+    expr = any(ConditionalExpr c).getCondition().getFullyConverted()
+    or
+    exists(Conversion cast | cast.getUnspecifiedType() instanceof BoolType | expr = cast.getExpr())
+  }
+
+  /**
+   * 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) {
+    // 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
+    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
+    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
+    or
+    // Case 3: the type of `expr` is not arithmetic. For example, it might
+    // be a pointer.
+    exprIsUsedAsBool(expr) and not exists(Util::exprMinVal(expr)) and result = 0
+  }
+
+  /**
+   * 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) {
+    // 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
+    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
+    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
+    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
+    or
+    // Case 3: the type of `expr` is not arithmetic. For example, it might
+    // be a pointer.
+    exprIsUsedAsBool(expr) and not exists(Util::exprMaxVal(expr)) and result = 1
+  }
+
+  /**
+   * This predicate computes the lower bounds of a phi definition. If the
+   * phi definition corresponds to a guard, then the guard is used to
+   * deduce a better lower bound.
+   * For example:
+   *
+   *     def:      x = y % 10;
+   *     guard:    if (x >= 2) {
+   *     block:      f(x)
+   *               }
+   *
+   * 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 |
+      phi.isGuardPhi(v, access, guard, branch) and
+      lowerBoundFromGuard(guard, access, guardLB, branch) and
+      defLB = getFullyConvertedLowerBounds(access)
+    |
+      // Compute the maximum of `guardLB` and `defLB`.
+      if guardLB > defLB then result = guardLB else result = defLB
+    )
+    or
+    exists(VariableAccess access, float neConstant, float lower |
+      isNEPhi(v, phi, access, neConstant) and
+      lower = getTruncatedLowerBounds(access) and
+      if lower = neConstant then result = lower + 1 else result = lower
+    )
+    or
+    exists(VariableAccess access |
+      isUnsupportedGuardPhi(v, phi, access) and
+      result = getTruncatedLowerBounds(access)
+    )
+    or
+    result = getDefLowerBounds(phi.getAPhiInput(v), v)
+  }
+
+  /** See comment for `getPhiLowerBounds`, above. */
+  private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
+    exists(VariableAccess access, Expr guard, boolean branch, float defUB, float guardUB |
+      phi.isGuardPhi(v, access, guard, branch) and
+      upperBoundFromGuard(guard, access, guardUB, branch) and
+      defUB = getFullyConvertedUpperBounds(access)
+    |
+      // Compute the minimum of `guardUB` and `defUB`.
+      if guardUB < defUB then result = guardUB else result = defUB
+    )
+    or
+    exists(VariableAccess access, float neConstant, float upper |
+      isNEPhi(v, phi, access, neConstant) and
+      upper = getTruncatedUpperBounds(access) and
+      if upper = neConstant then result = upper - 1 else result = upper
+    )
+    or
+    exists(VariableAccess access |
+      isUnsupportedGuardPhi(v, phi, access) and
+      result = getTruncatedUpperBounds(access)
+    )
+    or
+    result = getDefUpperBounds(phi.getAPhiInput(v), v)
+  }
+
+  /** Only to be called by `getDefLowerBounds`. */
+  private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
+    // Definitions with a defining value.
+    exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedLowerBounds(expr))
+    or
+    // Assignment operations with a defining value
+    exists(AssignOperation assignOp |
+      def = assignOp and
+      assignOp.getLValue() = v.getAnAccess() and
+      result = getTruncatedLowerBounds(assignOp)
+    )
+    or
+    exists(IncrementOperation incr, float newLB |
+      def = incr and
+      incr.getOperand() = v.getAnAccess() and
+      newLB = getFullyConvertedLowerBounds(incr.getOperand()) and
+      result = newLB + 1
+    )
+    or
+    exists(DecrementOperation decr, float newLB |
+      def = decr and
+      decr.getOperand() = v.getAnAccess() and
+      newLB = getFullyConvertedLowerBounds(decr.getOperand()) and
+      result = addRoundingDownSmall(newLB, -1)
+    )
+    or
+    // Phi nodes.
+    result = getPhiLowerBounds(v, def)
+    or
+    // Unanalyzable definitions.
+    unanalyzableDefBounds(def, v, result, _)
+  }
+
+  /** Only to be called by `getDefUpperBounds`. */
+  private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
+    // Definitions with a defining value.
+    exists(Expr expr | assignmentDef(def, v, expr) | result = getFullyConvertedUpperBounds(expr))
+    or
+    // Assignment operations with a defining value
+    exists(AssignOperation assignOp |
+      def = assignOp and
+      assignOp.getLValue() = v.getAnAccess() and
+      result = getTruncatedUpperBounds(assignOp)
+    )
+    or
+    exists(IncrementOperation incr, float newUB |
+      def = incr and
+      incr.getOperand() = v.getAnAccess() and
+      newUB = getFullyConvertedUpperBounds(incr.getOperand()) and
+      result = addRoundingUpSmall(newUB, 1)
+    )
+    or
+    exists(DecrementOperation decr, float newUB |
+      def = decr and
+      decr.getOperand() = v.getAnAccess() and
+      newUB = getFullyConvertedUpperBounds(decr.getOperand()) and
+      result = newUB - 1
+    )
+    or
+    // Phi nodes.
+    result = getPhiUpperBounds(v, def)
+    or
+    // Unanalyzable definitions.
+    unanalyzableDefBounds(def, v, _, result)
+  }
+
+  /**
+   * Helper for `getDefLowerBounds` and `getDefUpperBounds`. Find the set of
+   * unanalyzable definitions (such as function parameters) and make their
+   * bounds unknown.
+   */
+  private predicate unanalyzableDefBounds(
+    RangeSsaDefinition def, StackVariable v, float lb, float ub
+  ) {
+    v = def.getAVariable() and
+    not analyzableDef(def, v) and
+    lb = varMinVal(v) and
+    ub = varMaxVal(v)
+  }
+
+  /**
+   * Holds if in the `branch` branch of a guard `guard` involving `v`,
+   * we know that `v` is not NaN, and therefore it is safe to make range
+   * inferences about `v`.
+   */
+  bindingset[guard, v, branch]
+  predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
+    Util::getVariableRangeType(v.getTarget()) instanceof IntegralType
+    or
+    Util::getVariableRangeType(v.getTarget()) instanceof FloatingPointType and
+    v instanceof NonNanVariableAccess
+    or
+    // The reason the following case is here is to ensure that when we say
+    // `if (x > 5) { ...then... } else { ...else... }`
+    // it is ok to conclude that `x > 5` in the `then`, (though not safe
+    // to conclude that x <= 5 in `else`) even if we had no prior
+    // knowledge of `x` not being `NaN`.
+    nanExcludingComparison(guard, branch)
+  }
+
+  /**
+   * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
+   * 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, Util::RelationStrictness strictness |
+      boundFromGuard(guard, v, childLB, true, strictness, branch)
+    |
+      if nonNanGuardedVariable(guard, v, branch)
+      then
+        if
+          strictness = Util::Nonstrict() or
+          not Util::getVariableRangeType(v.getTarget()) instanceof IntegralType
+        then lb = childLB
+        else lb = childLB + 1
+      else lb = varMinVal(v.getTarget())
+    )
+  }
+
+  /**
+   * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
+   * 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, Util::RelationStrictness strictness |
+      boundFromGuard(guard, v, childUB, false, strictness, branch)
+    |
+      if nonNanGuardedVariable(guard, v, branch)
+      then
+        if
+          strictness = Util::Nonstrict() or
+          not Util::getVariableRangeType(v.getTarget()) instanceof IntegralType
+        then ub = childUB
+        else ub = childUB - 1
+      else ub = varMaxVal(v.getTarget())
+    )
+  }
+
+  /**
+   * This predicate simplifies the results returned by
+   * `linearBoundFromGuard`.
+   */
+  private predicate boundFromGuard(
+    Expr guard, VariableAccess v, float boundValue, boolean isLowerBound,
+    Util::RelationStrictness strictness, boolean branch
+  ) {
+    exists(float p, float q, float 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
+      or
+      p < 0 and isLowerBound = isLB.booleanNot()
+    )
+    or
+    // When `!e` is true, we know that `0 <= e <= 0`
+    exists(float p, float q, Expr e |
+      Util::linearAccess(e, v, p, q) and
+      Util::eqZeroWithNegate(guard, e, true, branch) and
+      boundValue = (0.0 - q) / p and
+      isLowerBound = [false, true] and
+      strictness = Util::Nonstrict()
+    )
+  }
+
+  /**
+   * This predicate finds guards of the form `p*v + q < r or p*v + q == r`
+   * and decomposes them into a tuple of values which can be used to deduce a
+   * 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?
+    Util::RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on?
+  ) {
+    // For the comparison x < RHS, we create two bounds:
+    //
+    //   1. x < upperbound(RHS)
+    //   2. x >= typeLowerBound(RHS.getUnspecifiedType())
+    //
+    exists(Expr lhs, Expr rhs, Util::RelationDirection dir, Util::RelationStrictness st |
+      Util::linearAccess(lhs, v, p, q) and
+      Util::relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch)
+    |
+      isLowerBound = Util::directionIsGreater(dir) and
+      strictness = st and
+      getBounds(rhs, boundValue, isLowerBound)
+      or
+      isLowerBound = Util::directionIsLesser(dir) and
+      strictness = Util::Nonstrict() and
+      exprTypeBounds(rhs, boundValue, isLowerBound)
+    )
+    or
+    // For x == RHS, we create the following bounds:
+    //
+    //   1. x <= upperbound(RHS)
+    //   2. x >= lowerbound(RHS)
+    //
+    exists(Expr lhs, Expr rhs |
+      Util::linearAccess(lhs, v, p, q) and
+      Util::eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
+      getBounds(rhs, boundValue, isLowerBound) and
+      strictness = Util::Nonstrict()
+    )
+    // x != RHS and !x are handled elsewhere
+  }
+
+  /** Utility for `linearBoundFromGuard`. */
+  private predicate getBounds(Expr expr, float 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) {
+    isLowerBound = true and boundValue = exprMinVal(expr.getFullyConverted())
+    or
+    isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted())
+  }
+
+  /**
+   * Holds if `(v, phi)` ensures that `access` is not equal to `neConstant`. For
+   * example, the condition `if (x + 1 != 3)` ensures that `x` is not equal to 2.
+   * Only integral types are supported.
+   */
+  private predicate isNEPhi(
+    Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant
+  ) {
+    exists(
+      ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q,
+      float r
+    |
+      phi.isGuardPhi(v, access, cmp, branch) and
+      Util::eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
+      v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
+      r = getValue(rExpr).toFloat() and
+      Util::linearAccess(linearExpr, access, p, q) and
+      neConstant = (r - q) / p
+    )
+    or
+    exists(Expr op, boolean branch, Expr linearExpr, float p, float q |
+      phi.isGuardPhi(v, access, op, branch) and
+      Util::eqZeroWithNegate(op, linearExpr, false, branch) and
+      v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise
+      Util::linearAccess(linearExpr, access, p, q) and
+      neConstant = (0.0 - q) / p
+    )
+  }
+
+  /**
+   * Holds if `(v, phi)` constrains the value of `access` but in a way that
+   * doesn't allow this library to constrain the upper or lower bounds of
+   * `access`. An example is `if (x != y)` if neither `x` nor `y` is a
+   * compile-time constant.
+   */
+  private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, VariableAccess access) {
+    exists(Expr cmp, boolean branch |
+      Util::eqOpWithSwapAndNegate(cmp, _, _, false, branch)
+      or
+      Util::eqZeroWithNegate(cmp, _, false, branch)
+    |
+      phi.isGuardPhi(v, access, cmp, branch) and
+      not isNEPhi(v, phi, access, _)
+    )
+  }
+
+  /**
+   * Gets the upper bound of the expression, if the expression is guarded.
+   * 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) {
+    exists(
+      RangeSsaDefinition def, StackVariable v, VariableAccess guardVa, Expr guard, boolean branch
+    |
+      def.isGuardPhi(v, guardVa, guard, branch) and
+      // If the basic block for the variable access being examined has
+      // more than one predecessor, the guard phi node could originate
+      // from one of the predecessors. This is because the guard phi
+      // node is attached to the block at the end of the edge and not on
+      // the actual edge. It is therefore not possible to determine which
+      // edge the guard phi node belongs to. The predicate below ensures
+      // 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
+      not convertedExprMightOverflow(guard.getAChild+())
+    )
+  }
+
+  cached
+  private module SimpleRangeAnalysisCached {
+    /**
+     * Gets the lower bound of the expression.
+     *
+     * Note: expressions in C/C++ are often implicitly or explicitly cast to a
+     * different result type. Such casts can cause the value of the expression
+     * to overflow or to be truncated. This predicate computes the lower bound
+     * of the expression without including the effect of the casts. To compute
+     * the lower bound of the expression after all the casts have been applied,
+     * call `lowerBound` like this:
+     *
+     *    `lowerBound(expr.getFullyConverted())`
+     */
+    cached
+    float lowerBound(Expr expr) {
+      // Combine the lower bounds returned by getTruncatedLowerBounds into a
+      // single minimum value.
+      result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb)
+    }
+
+    /**
+     * Gets the upper bound of the expression.
+     *
+     * Note: expressions in C/C++ are often implicitly or explicitly cast to a
+     * different result type. Such casts can cause the value of the expression
+     * to overflow or to be truncated. This predicate computes the upper bound
+     * of the expression without including the effect of the casts. To compute
+     * the upper bound of the expression after all the casts have been applied,
+     * call `upperBound` like this:
+     *
+     *    `upperBound(expr.getFullyConverted())`
+     */
+    cached
+    float upperBound(Expr expr) {
+      // Combine the upper bounds returned by getTruncatedUpperBounds and
+      // getGuardedUpperBound into a single maximum value
+      result = min([max(getTruncatedUpperBounds(expr)), getGuardedUpperBound(expr)])
+    }
+
+    /** Holds if the upper bound of `expr` may have been widened. This means the upper bound is in practice likely to be overly wide. */
+    cached
+    predicate upperBoundMayBeWidened(Expr e) {
+      isRecursiveExpr(e) and
+      // Widening is not a problem if the post-analysis in `getGuardedUpperBound` has overridden the widening.
+      // Note that the RHS of `<` may be multi-valued.
+      not getGuardedUpperBound(e) < getTruncatedUpperBounds(e)
+    }
+
+    /**
+     * Holds if `expr` has a provably empty range. For example:
+     *
+     *   10 < expr and expr < 5
+     *
+     * The range of an expression can only be empty if it can never be
+     * executed. For example:
+     *
+     *   if (10 < x) {
+     *     if (x < 5) {
+     *       // Unreachable code
+     *       return x; // x has an empty range: 10 < x && x < 5
+     *     }
+     *   }
+     */
+    cached
+    predicate exprWithEmptyRange(Expr expr) {
+      analyzableExpr(expr) and
+      (
+        not exists(lowerBound(expr)) or
+        not exists(upperBound(expr)) or
+        lowerBound(expr) > upperBound(expr)
+      )
+    }
+
+    /** Holds if the definition might overflow negatively. */
+    cached
+    predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) {
+      getDefLowerBoundsImpl(def, v) < Util::varMinVal(v)
+    }
+
+    /** Holds if the definition might overflow positively. */
+    cached
+    predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) {
+      getDefUpperBoundsImpl(def, v) > Util::varMaxVal(v)
+    }
+
+    /**
+     * Holds if the definition might overflow (either positively or
+     * negatively).
+     */
+    cached
+    predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
+      defMightOverflowNegatively(def, v) or
+      defMightOverflowPositively(def, v)
+    }
+
+    /**
+     * Holds if `e` is an expression where the concept of overflow makes sense.
+     * This predicate is used to filter out some of the unanalyzable expressions
+     * from `exprMightOverflowPositively` and `exprMightOverflowNegatively`.
+     */
+    pragma[inline]
+    private predicate exprThatCanOverflow(Expr e) {
+      e instanceof UnaryArithmeticOperation or
+      e instanceof BinaryArithmeticOperation or
+      e instanceof AssignArithmeticOperation or
+      e instanceof LShiftExpr or
+      e instanceof AssignLShiftExpr
+    }
+
+    /**
+     * Holds if the expression might overflow negatively. This predicate
+     * does not consider the possibility that the expression might overflow
+     * due to a conversion.
+     */
+    cached
+    predicate exprMightOverflowNegatively(Expr expr) {
+      getLowerBoundsImpl(expr) < Util::exprMinVal(expr)
+      or
+      // The lower bound of the expression `x--` is the same as the lower
+      // bound of `x`, so the standard logic (above) does not work for
+      // detecting whether it might overflow.
+      getLowerBoundsImpl(expr.(PostfixDecrExpr)) = Util::exprMinVal(expr)
+      or
+      // We can't conclude that any unanalyzable expression might overflow. This
+      // is because there are many expressions that the range analysis doesn't
+      // handle, but where the concept of overflow doesn't make sense.
+      exprThatCanOverflow(expr) and not analyzableExpr(expr)
+    }
+
+    /**
+     * Holds if the expression might overflow negatively. Conversions
+     * are also taken into account. For example the expression
+     * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
+     * due to the addition.
+     */
+    cached
+    predicate convertedExprMightOverflowNegatively(Expr expr) {
+      exprMightOverflowNegatively(expr) or
+      convertedExprMightOverflowNegatively(expr.getConversion())
+    }
+
+    /**
+     * Holds if the expression might overflow positively. This predicate
+     * does not consider the possibility that the expression might overflow
+     * due to a conversion.
+     */
+    cached
+    predicate exprMightOverflowPositively(Expr expr) {
+      getUpperBoundsImpl(expr) > Util::exprMaxVal(expr)
+      or
+      // The upper bound of the expression `x++` is the same as the upper
+      // bound of `x`, so the standard logic (above) does not work for
+      // detecting whether it might overflow.
+      getUpperBoundsImpl(expr.(PostfixIncrExpr)) = Util::exprMaxVal(expr)
+    }
+
+    /**
+     * Holds if the expression might overflow positively. Conversions
+     * are also taken into account. For example the expression
+     * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
+     * due to the addition.
+     */
+    cached
+    predicate convertedExprMightOverflowPositively(Expr expr) {
+      exprMightOverflowPositively(expr) or
+      convertedExprMightOverflowPositively(expr.getConversion())
+    }
+
+    /**
+     * Holds if the expression might overflow (either positively or
+     * negatively). The possibility that the expression might overflow
+     * due to an implicit or explicit cast is also considered.
+     */
+    cached
+    predicate convertedExprMightOverflow(Expr expr) {
+      convertedExprMightOverflowNegatively(expr) or
+      convertedExprMightOverflowPositively(expr)
+    }
+  }
+
+  /**
+   * Gets the truncated lower bounds of the fully converted expression.
+   */
+  float getFullyConvertedLowerBounds(Expr expr) {
+    result = getTruncatedLowerBounds(expr.getFullyConverted())
+  }
+
+  /**
+   * Gets the truncated upper bounds of the fully converted expression.
+   */
+  float getFullyConvertedUpperBounds(Expr expr) {
+    result = getTruncatedUpperBounds(expr.getFullyConverted())
+  }
+
+  /**
+   * Get the lower bounds for a `RangeSsaDefinition`. Most of the work is
+   * 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 |
+      newLB = getDefLowerBoundsImpl(def, v) and
+      if Util::varMinVal(v) <= newLB and newLB <= Util::varMaxVal(v)
+      then truncatedLB = newLB
+      else truncatedLB = Util::varMinVal(v)
+    |
+      // Widening: check whether the new lower bound is from a source which
+      // depends recursively on the current definition.
+      if isRecursiveDef(def, v)
+      then
+        // The new lower bound is from a recursive source, so we round
+        // down to one of a limited set of values to prevent the
+        // recursion from exploding.
+        result =
+          max(float widenLB |
+            widenLB = wideningLowerBounds(Util::getVariableRangeType(v)) and
+            not widenLB > truncatedLB
+          |
+            widenLB
+          )
+      else result = truncatedLB
+    )
+    or
+    // The definition might overflow positively and wrap. If so, the lower
+    // bound is `typeLowerBound`.
+    defMightOverflowPositively(def, v) and result = Util::varMinVal(v)
+  }
+
+  /** See comment for `getDefLowerBounds`, above. */
+  float getDefUpperBounds(RangeSsaDefinition def, StackVariable v) {
+    exists(float newUB, float truncatedUB |
+      newUB = getDefUpperBoundsImpl(def, v) and
+      if Util::varMinVal(v) <= newUB and newUB <= Util::varMaxVal(v)
+      then truncatedUB = newUB
+      else truncatedUB = Util::varMaxVal(v)
+    |
+      // Widening: check whether the new upper bound is from a source which
+      // depends recursively on the current definition.
+      if isRecursiveDef(def, v)
+      then
+        // The new upper bound is from a recursive source, so we round
+        // up to one of a fixed set of values to prevent the recursion
+        // from exploding.
+        result =
+          min(float widenUB |
+            widenUB = wideningUpperBounds(Util::getVariableRangeType(v)) and
+            not widenUB < truncatedUB
+          |
+            widenUB
+          )
+      else result = truncatedUB
+    )
+    or
+    // The definition might overflow negatively and wrap. If so, the upper
+    // bound is `typeUpperBound`.
+    defMightOverflowNegatively(def, v) and result = Util::varMaxVal(v)
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll
new file mode 100644
index 000000000..7cdc6430a
--- /dev/null
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/FloatingTypes2.qll
@@ -0,0 +1,44 @@
+//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY.  **/
+import cpp
+import RuleMetadata
+import codingstandards.cpp.exclusions.RuleMetadata
+
+newtype FloatingTypes2Query =
+  TPossibleMisuseOfUndetectedInfinityQuery() or
+  TPossibleMisuseOfUndetectedNaNQuery()
+
+predicate isFloatingTypes2QueryMetadata(Query query, string queryId, string ruleId, string category) {
+  query =
+    // `Query` instance for the `possibleMisuseOfUndetectedInfinity` query
+    FloatingTypes2Package::possibleMisuseOfUndetectedInfinityQuery() and
+  queryId =
+    // `@id` for the `possibleMisuseOfUndetectedInfinity` query
+    "c/misra/possible-misuse-of-undetected-infinity" and
+  ruleId = "DIR-4-15" and
+  category = "required"
+  or
+  query =
+    // `Query` instance for the `possibleMisuseOfUndetectedNaN` query
+    FloatingTypes2Package::possibleMisuseOfUndetectedNaNQuery() and
+  queryId =
+    // `@id` for the `possibleMisuseOfUndetectedNaN` query
+    "c/misra/possible-misuse-of-undetected-na-n" and
+  ruleId = "DIR-4-15" and
+  category = "required"
+}
+
+module FloatingTypes2Package {
+  Query possibleMisuseOfUndetectedInfinityQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `possibleMisuseOfUndetectedInfinity` query
+      TQueryC(TFloatingTypes2PackageQuery(TPossibleMisuseOfUndetectedInfinityQuery()))
+  }
+
+  Query possibleMisuseOfUndetectedNaNQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `possibleMisuseOfUndetectedNaN` query
+      TQueryC(TFloatingTypes2PackageQuery(TPossibleMisuseOfUndetectedNaNQuery()))
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
index 6ab695fb9..41ae2931b 100644
--- a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
+++ b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll
@@ -32,6 +32,7 @@ import Declarations8
 import EssentialTypes
 import Expressions
 import FloatingTypes
+import FloatingTypes2
 import FunctionTypes
 import IO1
 import IO2
@@ -112,6 +113,7 @@ newtype TCQuery =
   TEssentialTypesPackageQuery(EssentialTypesQuery q) or
   TExpressionsPackageQuery(ExpressionsQuery q) or
   TFloatingTypesPackageQuery(FloatingTypesQuery q) or
+  TFloatingTypes2PackageQuery(FloatingTypes2Query q) or
   TFunctionTypesPackageQuery(FunctionTypesQuery q) or
   TIO1PackageQuery(IO1Query q) or
   TIO2PackageQuery(IO2Query q) or
@@ -192,6 +194,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
   isEssentialTypesQueryMetadata(query, queryId, ruleId, category) or
   isExpressionsQueryMetadata(query, queryId, ruleId, category) or
   isFloatingTypesQueryMetadata(query, queryId, ruleId, category) or
+  isFloatingTypes2QueryMetadata(query, queryId, ruleId, category) or
   isFunctionTypesQueryMetadata(query, queryId, ruleId, category) or
   isIO1QueryMetadata(query, queryId, ruleId, category) or
   isIO2QueryMetadata(query, queryId, ruleId, category) or
diff --git a/rule_packages/c/FloatingTypes2.json b/rule_packages/c/FloatingTypes2.json
new file mode 100644
index 000000000..3f4771dcc
--- /dev/null
+++ b/rule_packages/c/FloatingTypes2.json
@@ -0,0 +1,36 @@
+{
+  "MISRA-C-2012": {
+    "DIR-4-15": {
+      "properties": {
+        "obligation": "required"
+      },
+      "queries": [
+        {
+          "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities.",
+          "kind": "path-problem",
+          "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities",
+          "precision": "medium",
+          "severity": "warning",
+          "short_name": "PossibleMisuseOfUndetectedInfinity",
+          "tags": [
+            "correctness",
+            "external/misra/c/2012/amendment3"
+          ]
+        },
+        {
+          "description": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs.",
+          "kind": "path-problem",
+          "name": "Evaluation of floating-point expressions shall not lead to the undetected generation of NaNs",
+          "precision": "low",
+          "severity": "warning",
+          "short_name": "PossibleMisuseOfUndetectedNaN",
+          "tags": [
+            "correctness",
+            "external/misra/c/2012/amendment3"
+          ]
+        }
+      ],
+      "title": "Evaluation of floating-point expressions shall not lead to the undetected generation of infinities and NaNs"
+    }
+  }
+}
\ No newline at end of file