@@ -111,19 +111,6 @@ private module Impl {
111111 }
112112 }
113113
114- private Guard eqFlowCondAbs (
115- Definition def , ExprNode e , int delta , boolean isEq , G:: AbstractValue v
116- ) {
117- exists ( boolean eqpolarity |
118- result .isEquality ( ssaRead ( def , delta ) , e , eqpolarity ) and
119- eqpolarity .booleanXor ( v .( BooleanValue ) .getValue ( ) ) .booleanNot ( ) = isEq
120- )
121- or
122- exists ( G:: AbstractValue v0 |
123- G:: Internal:: impliesStep ( result , v , eqFlowCondAbs ( def , e , delta , isEq , v0 ) , v0 )
124- )
125- }
126-
127114 /**
128115 * Gets a condition that tests whether `def` equals `e + delta`.
129116 *
@@ -132,9 +119,10 @@ private module Impl {
132119 * - `isEq = false` : `def != e + delta`
133120 */
134121 Guard eqFlowCond ( Definition def , ExprNode e , int delta , boolean isEq , boolean testIsTrue ) {
135- exists ( BooleanValue v |
136- result = eqFlowCondAbs ( def , e , delta , isEq , v ) and
137- testIsTrue = v .getValue ( )
122+ exists ( boolean eqpolarity |
123+ result .isEquality ( ssaRead ( def , delta ) , e , eqpolarity ) and
124+ testIsTrue = [ false , true ] and
125+ eqpolarity .booleanXor ( testIsTrue ) .booleanNot ( ) = isEq
138126 )
139127 }
140128
0 commit comments