@@ -102,27 +102,34 @@ abstract private class GuardConditionImpl extends Expr {
102
102
this .valueControls ( controlled , any ( BooleanValue bv | bv .getValue ( ) = testIsTrue ) )
103
103
}
104
104
105
- /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
105
+ /**
106
+ * Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this
107
+ * expression evaluates to `testIsTrue`. Note that there's a 4-argument
108
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
109
+ */
106
110
pragma [ inline]
107
111
abstract predicate comparesLt ( Expr left , Expr right , int k , boolean isLessThan , boolean testIsTrue ) ;
108
112
109
113
/**
110
114
* Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
111
- * If `isLessThan = false` then this implies `left >= right + k`.
115
+ * If `isLessThan = false` then this implies `left >= right + k`. Note that there's a 4-argument
116
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
112
117
*/
113
118
pragma [ inline]
114
119
abstract predicate ensuresLt ( Expr left , Expr right , int k , BasicBlock block , boolean isLessThan ) ;
115
120
116
121
/**
117
122
* Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
118
- * this expression evaluates to `value`.
123
+ * this expression evaluates to `value`. Note that there's a 4-argument
124
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
119
125
*/
120
126
pragma [ inline]
121
127
abstract predicate comparesLt ( Expr e , int k , boolean isLessThan , AbstractValue value ) ;
122
128
123
129
/**
124
130
* Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
125
- * If `isLessThan = false` then this implies `e >= k`.
131
+ * If `isLessThan = false` then this implies `e >= k`. Note that there's a 4-argument
132
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
126
133
*/
127
134
pragma [ inline]
128
135
abstract predicate ensuresLt ( Expr e , int k , BasicBlock block , boolean isLessThan ) ;
@@ -142,7 +149,8 @@ abstract private class GuardConditionImpl extends Expr {
142
149
143
150
/**
144
151
* Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
145
- * If `areEqual = false` then this implies `left != right + k`.
152
+ * If `areEqual = false` then this implies `left != right + k`. Note that there's a 4-argument
153
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
146
154
*/
147
155
pragma [ inline]
148
156
abstract predicate ensuresEq ( Expr left , Expr right , int k , BasicBlock block , boolean areEqual ) ;
@@ -162,7 +170,8 @@ abstract private class GuardConditionImpl extends Expr {
162
170
163
171
/**
164
172
* Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
165
- * If `areEqual = false` then this implies `e != k`.
173
+ * If `areEqual = false` then this implies `e != k`. Note that there's a 4-argument
174
+ * ("unary") and a 5-argument ("binary") version of this predicate (see `comparesEq`).
166
175
*/
167
176
pragma [ inline]
168
177
abstract predicate ensuresEq ( Expr e , int k , BasicBlock block , boolean areEqual ) ;
0 commit comments