@@ -1130,10 +1130,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11301130 private module StatefulWrapper = ValidationWrapperWithState< Unit , guardChecksWithState / 4 > ;
11311131
11321132 /**
1133- * Holds if the guard `g` validates the expression `e ` upon evaluating to `val`.
1133+ * Holds if the guard `g` validates the SSA definition `def ` upon evaluating to `val`.
11341134 */
1135- predicate guardChecks ( Guard g , Expr e , GuardValue val ) {
1136- StatefulWrapper:: guardChecks ( g , e , val , _)
1135+ predicate guardChecksDef ( Guard g , SsaDefinition def , GuardValue val ) {
1136+ StatefulWrapper:: guardChecksDef ( g , def , val , _)
11371137 }
11381138 }
11391139
@@ -1156,7 +1156,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11561156 exists ( NonOverridableMethod m , SsaDefinition param , Guard guard , GuardValue val |
11571157 m .getAReturnExpr ( ) = ret and
11581158 parameterDefinition ( m .getParameter ( ppos ) , param ) and
1159- guardChecks ( guard , param . getARead ( ) , val , state )
1159+ guardChecksDef ( guard , param , val , state )
11601160 |
11611161 guard .valueControls ( ret .getBasicBlock ( ) , val ) and
11621162 relevantReturnValue ( m , retval )
@@ -1185,7 +1185,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11851185 or
11861186 exists ( SsaDefinition param , BasicBlock bb , Guard guard , GuardValue val |
11871187 parameterDefinition ( result .getParameter ( ppos ) , param ) and
1188- guardChecks ( guard , param . getARead ( ) , val , state ) and
1188+ guardChecksDef ( guard , param , val , state ) and
11891189 guard .valueControls ( bb , val ) and
11901190 normalExitBlock ( bb ) and
11911191 retval = TException ( false )
@@ -1195,7 +1195,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
11951195 /**
11961196 * Holds if the guard `g` validates the expression `e` upon evaluating to `val`.
11971197 */
1198- predicate guardChecks ( Guard g , Expr e , GuardValue val , State state ) {
1198+ private predicate guardChecks ( Guard g , Expr e , GuardValue val , State state ) {
11991199 guardChecks0 ( g , e , val .asBooleanValue ( ) , state )
12001200 or
12011201 exists ( NonOverridableMethodCall call , ParameterPosition ppos , ArgumentPosition apos |
@@ -1205,6 +1205,16 @@ module Make<LocationSig Location, InputSig<Location> Input> {
12051205 parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) )
12061206 )
12071207 }
1208+
1209+ /**
1210+ * Holds if the guard `g` validates the SSA definition `def` upon evaluating to `val`.
1211+ */
1212+ predicate guardChecksDef ( Guard g , SsaDefinition def , GuardValue val , State state ) {
1213+ exists ( Expr e |
1214+ guardChecks ( g , e , val , state ) and
1215+ guardReadsSsaVar ( e , def )
1216+ )
1217+ }
12081218 }
12091219
12101220 /**
0 commit comments