@@ -1163,25 +1163,22 @@ abstract class BarrierGuard extends Node {
11631163 * Holds if `guard` markes a point in the control-flow graph where this node
11641164 * is known to validate `nd`.
11651165 */
1166- pragma [ noopt]
11671166 private predicate guards ( ControlFlow:: ConditionGuardNode guard , Node nd ) {
1168- exists ( boolean branch , Expr expr |
1169- expr = nd .asExpr ( ) and
1170- this .checks ( expr , branch ) and
1167+ exists ( boolean branch |
1168+ this .checks ( nd .asExpr ( ) , branch ) and
11711169 guard .ensures ( this , branch )
11721170 )
11731171 or
11741172 exists (
11751173 Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , CallNode c ,
1176- Node resNode , Node check , boolean outcome , Node functionOutput
1174+ Node resNode , Node check , boolean outcome
11771175 |
11781176 guardingFunction ( f , inp , outp , p ) and
11791177 c = f .getACall ( ) and
11801178 nd = inp .getNode ( c ) and
1181- functionOutput = outp .getNode ( c ) and
1182- localFlow ( functionOutput , resNode ) and
1179+ localFlow ( pragma [ only_bind_into ] ( outp .getNode ( c ) ) , resNode ) and
11831180 p .checkOn ( check , outcome , resNode ) and
1184- guard .ensures ( check , outcome )
1181+ guard .ensures ( pragma [ only_bind_into ] ( check ) , outcome )
11851182 )
11861183 }
11871184
0 commit comments