@@ -127,7 +127,16 @@ abstract private class GuardConditionImpl extends Expr {
127
127
pragma [ inline]
128
128
abstract predicate ensuresLt ( Expr e , int k , BasicBlock block , boolean isLessThan ) ;
129
129
130
- /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
130
+ /**
131
+ * Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this
132
+ * expression evaluates to `testIsTrue`. Note that there's a 4-argument ("unary") and a
133
+ * 5-argument ("binary") version of `comparesEq` and they are not equivalent:
134
+ * - the unary version is suitable for guards where there is no expression representing the
135
+ * right-hand side, such as `if (x)`, and also works for equality with an integer constant
136
+ * (such as `if (x == k)`).
137
+ * - the binary version is the more general case for comparison of any expressions (not
138
+ * necessarily integer).
139
+ */
131
140
pragma [ inline]
132
141
abstract predicate comparesEq ( Expr left , Expr right , int k , boolean areEqual , boolean testIsTrue ) ;
133
142
@@ -138,7 +147,16 @@ abstract private class GuardConditionImpl extends Expr {
138
147
pragma [ inline]
139
148
abstract predicate ensuresEq ( Expr left , Expr right , int k , BasicBlock block , boolean areEqual ) ;
140
149
141
- /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */
150
+ /**
151
+ * Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression
152
+ * evaluates to `value`. Note that there's a 4-argument ("unary") and a 5-argument ("binary")
153
+ * version of `comparesEq` and they are not equivalent:
154
+ * - the unary version is suitable for guards where there is no expression representing the
155
+ * right-hand side, such as `if (x)`, and also works for equality with an integer constant
156
+ * (such as `if (x == k)`).
157
+ * - the binary version is the more general case for comparison of any expressions (not
158
+ * necessarily integer).
159
+ */
142
160
pragma [ inline]
143
161
abstract predicate comparesEq ( Expr e , int k , boolean areEqual , AbstractValue value ) ;
144
162
0 commit comments