1+ /**
2+ * Provides an AST-based interface to the relative range analysis, which tracks bounds of the form
3+ * `a < B + delta` for expressions `a` and `b` and an integer offset `delta`.
4+ */
5+
16private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
27private import cpp
38private import semmle.code.cpp.ir.IR
@@ -14,13 +19,22 @@ private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
1419predicate bounded ( Expr e , Bound b , float delta , boolean upper , Reason reason ) {
1520 exists ( SemanticExprConfig:: Expr semExpr |
1621 semExpr .getUnconverted ( ) .getUnconvertedResultExpression ( ) = e
17- or
18- semExpr .getConverted ( ) .getConvertedResultExpression ( ) = e
1922 |
2023 semBounded ( semExpr , b , delta , upper , reason )
2124 )
2225}
2326
27+ /**
28+ * Holds if e is bounded by `b + delta`. The bound is an upper bound if
29+ * `upper` is true, and can be traced baack to a guard represented by `reason`.
30+ */
31+ predicate convertedBounded ( Expr e , Bound b , float delta , boolean upper , Reason reason ) {
32+ exists ( SemanticExprConfig:: Expr semExpr |
33+ semExpr .getConverted ( ) .getConvertedResultExpression ( ) = e
34+ |
35+ semBounded ( semExpr , b , delta , upper , reason )
36+ )
37+ }
2438/**
2539 * A reason for an inferred bound. This can either be `CondReason` if the bound
2640 * is due to a specific condition, or `NoReason` if the bound is inferred
0 commit comments