@@ -0,0 +1,120 @@
+/**
+ * Wrapper for the semantic range analysis library that mimics the
+ * interface of the simple range analysis library.
+ */
+
+private import cpp
+private import semmle.code.cpp.ir.IR
+private import experimental.semmle.code.cpp.semantic.SemanticBound
+private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
+private import RangeAnalysis
+
+/**
+ * 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())`
+ */
+float lowerBound(Expr expr) {
+  exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
+    semBounded(getSemanticExpr(i), b, result, false, _)
+  )
+}
+
+/**
+ * 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())`
+ */
+float upperBound(Expr expr) {
+  exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
+    semBounded(getSemanticExpr(i), b, result, true, _)
+  )
+}
+
+/**
+ * Holds if the upper bound of `expr` may have been widened. This means the
+ * upper bound is in practice likely to be overly wide.
+ */
+predicate upperBoundMayBeWidened(Expr e) { none() }
+
+/**
+ * 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:
+ *
+ * ```cpp
+ * if (10 < x) {
+ *   if (x < 5) {
+ *     // Unreachable code
+ *     return x; // x has an empty range: 10 < x && x < 5
+ *   }
+ * }
+ * ```
+ */
+predicate exprWithEmptyRange(Expr expr) { lowerBound(expr) > upperBound(expr) }
+
+/** Holds if the definition might overflow negatively. */
+predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) { none() }
+
+/** Holds if the definition might overflow positively. */
+predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) { none() }
+
+/**
+ * Holds if the definition might overflow (either positively or
+ * negatively).
+ */
+predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) { none() }
+
+/**
+ * Holds if the expression might overflow negatively. This predicate
+ * does not consider the possibility that the expression might overflow
+ * due to a conversion.
+ */
+predicate exprMightOverflowNegatively(Expr expr) { none() }
+
+/**
+ * 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.
+ */
+predicate convertedExprMightOverflowNegatively(Expr expr) { none() }
+
+/**
+ * Holds if the expression might overflow positively. This predicate
+ * does not consider the possibility that the expression might overflow
+ * due to a conversion.
+ */
+predicate exprMightOverflowPositively(Expr expr) { none() }
+
+/**
+ * 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.
+ */
+predicate convertedExprMightOverflowPositively(Expr expr) { none() }
+
+/**
+ * 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.
+ */
+predicate convertedExprMightOverflow(Expr expr) { none() }