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
+
1
6
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
2
7
private import cpp
3
8
private import semmle.code.cpp.ir.IR
@@ -14,13 +19,22 @@ private import semmle.code.cpp.valuenumbering.GlobalValueNumbering
14
19
predicate bounded ( Expr e , Bound b , float delta , boolean upper , Reason reason ) {
15
20
exists ( SemanticExprConfig:: Expr semExpr |
16
21
semExpr .getUnconverted ( ) .getUnconvertedResultExpression ( ) = e
17
- or
18
- semExpr .getConverted ( ) .getConvertedResultExpression ( ) = e
19
22
|
20
23
semBounded ( semExpr , b , delta , upper , reason )
21
24
)
22
25
}
23
26
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
+ }
24
38
/**
25
39
* A reason for an inferred bound. This can either be `CondReason` if the bound
26
40
* is due to a specific condition, or `NoReason` if the bound is inferred
0 commit comments