Rangeanalysis: Rename predicate.

This commit is contained in:
Anders Schack-Mulligen
2023-11-10 15:17:13 +01:00
parent f05b75e04f
commit 30aefabb2a
4 changed files with 8 additions and 8 deletions

View File

@@ -22,7 +22,7 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() } predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
/** /**
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
} }

View File

@@ -54,7 +54,7 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() } predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
/** /**
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
} }

View File

@@ -332,7 +332,7 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
/** /**
* Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate hasBound(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) { predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) {
exists(RandomDataSource rds | exists(RandomDataSource rds |
e2 = rds.getOutput() and e2 = rds.getOutput() and
( (

View File

@@ -270,9 +270,9 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
predicate hasConstantBound(Sem::Expr e, D::Delta bound, boolean upper); predicate hasConstantBound(Sem::Expr e, D::Delta bound, boolean upper);
/** /**
* Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate hasBound(Sem::Expr e, Sem::Expr bound, D::Delta delta, boolean upper); predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper);
/** /**
* Ignore the bound on this expression. * Ignore the bound on this expression.
@@ -740,7 +740,7 @@ module RangeStage<
delta = D::fromInt(0) and delta = D::fromInt(0) and
upper = false upper = false
or or
hasBound(e2, e1, delta, upper) additionalBoundFlowStep(e2, e1, delta, upper)
} }
/** Holds if `e2 = e1 * factor` and `factor > 0`. */ /** Holds if `e2 = e1 * factor` and `factor > 0`. */