@@ -131,8 +131,10 @@ module Barrier2 {
131131 }
132132
133133 Instruction getABarrierInstruction ( FlowState2 state ) {
134- exists ( IRGuardCondition g , ValueNumber value , boolean edge |
135- operandGuardChecks ( g , value .getAUse ( ) , _, state , edge ) and
134+ exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge |
135+ use = value .getAUse ( ) and
136+ operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) , _,
137+ pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( edge ) ) and
136138 result = value .getAnInstruction ( ) and
137139 g .controls ( result .getBlock ( ) , edge )
138140 )
@@ -239,11 +241,13 @@ pragma[nomagic]
239241predicate pointerAddInstructionHasBounds (
240242 PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
241243) {
242- exists ( Instruction right |
244+ exists ( Instruction right , Instruction instr2 |
243245 pai .getRight ( ) = right and
244246 pai .getLeft ( ) = sink1 .asInstruction ( ) and
245- bounded1 ( right , sink2 .asInstruction ( ) , delta ) and
246- not [ right , sink2 .asInstruction ( ) ] = Barrier2:: getABarrierInstruction ( delta )
247+ instr2 = sink2 .asInstruction ( ) and
248+ bounded1 ( right , instr2 , delta ) and
249+ not right = Barrier2:: getABarrierInstruction ( delta ) and
250+ not instr2 = Barrier2:: getABarrierInstruction ( delta )
247251 )
248252}
249253
0 commit comments