@@ -1285,39 +1285,35 @@ module IsUnreachableInCall {
12851285 predicate isUnreachableInCall ( NodeRegion block , DataFlowCall call ) {
12861286 exists (
12871287 InstructionDirectParameterNode paramNode , ConstantIntegralTypeArgumentNode arg ,
1288- IntegerConstantInstruction constant , int k , Operand left , Operand right
1288+ IntegerConstantInstruction constant , int k , Operand left , Operand right , int argval
12891289 |
12901290 // arg flows into `paramNode`
1291- DataFlowImplCommon:: viableParamArg ( call , paramNode , arg ) and
1291+ DataFlowImplCommon:: viableParamArg ( call , pragma [ only_bind_into ] ( paramNode ) ,
1292+ pragma [ only_bind_into ] ( arg ) ) and
12921293 left = constant .getAUse ( ) and
1293- right = valueNumber ( paramNode .getInstruction ( ) ) .getAUse ( )
1294+ right = valueNumber ( paramNode .getInstruction ( ) ) .getAUse ( ) and
1295+ argval = arg .getValue ( )
12941296 |
12951297 // and there's a guard condition which ensures that the result of `left == right + k` is `areEqual`
1296- exists ( boolean areEqual |
1297- ensuresEq ( pragma [ only_bind_into ] ( left ) , pragma [ only_bind_into ] ( right ) ,
1298- pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( block ) , areEqual )
1299- |
1298+ exists ( boolean areEqual | ensuresEq ( left , right , k , block , areEqual ) |
13001299 // this block ensures that left = right + k, but it holds that `left != right + k`
13011300 areEqual = true and
1302- constant .getValue ( ) .toInt ( ) != arg . getValue ( ) + k
1301+ constant .getValue ( ) .toInt ( ) != argval + k
13031302 or
13041303 // this block ensures that or `left != right + k`, but it holds that `left = right + k`
13051304 areEqual = false and
1306- constant .getValue ( ) .toInt ( ) = arg . getValue ( ) + k
1305+ constant .getValue ( ) .toInt ( ) = argval + k
13071306 )
13081307 or
13091308 // or there's a guard condition which ensures that the result of `left < right + k` is `isLessThan`
1310- exists ( boolean isLessThan |
1311- ensuresLt ( pragma [ only_bind_into ] ( left ) , pragma [ only_bind_into ] ( right ) ,
1312- pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( block ) , isLessThan )
1313- |
1309+ exists ( boolean isLessThan | ensuresLt ( left , right , k , block , isLessThan ) |
13141310 isLessThan = true and
13151311 // this block ensures that `left < right + k`, but it holds that `left >= right + k`
1316- constant .getValue ( ) .toInt ( ) >= arg . getValue ( ) + k
1312+ constant .getValue ( ) .toInt ( ) >= argval + k
13171313 or
13181314 // this block ensures that `left >= right + k`, but it holds that `left < right + k`
13191315 isLessThan = false and
1320- constant .getValue ( ) .toInt ( ) < arg . getValue ( ) + k
1316+ constant .getValue ( ) .toInt ( ) < argval + k
13211317 )
13221318 )
13231319 }
0 commit comments