@@ -127,7 +127,16 @@ abstract private class GuardConditionImpl extends Expr {
127127 pragma [ inline]
128128 abstract predicate ensuresLt ( Expr e , int k , BasicBlock block , boolean isLessThan ) ;
129129
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+ */
131140 pragma [ inline]
132141 abstract predicate comparesEq ( Expr left , Expr right , int k , boolean areEqual , boolean testIsTrue ) ;
133142
@@ -138,7 +147,16 @@ abstract private class GuardConditionImpl extends Expr {
138147 pragma [ inline]
139148 abstract predicate ensuresEq ( Expr left , Expr right , int k , BasicBlock block , boolean areEqual ) ;
140149
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+ */
142160 pragma [ inline]
143161 abstract predicate comparesEq ( Expr e , int k , boolean areEqual , AbstractValue value ) ;
144162
0 commit comments