@@ -1285,39 +1285,35 @@ module IsUnreachableInCall {
1285
1285
predicate isUnreachableInCall ( NodeRegion block , DataFlowCall call ) {
1286
1286
exists (
1287
1287
InstructionDirectParameterNode paramNode , ConstantIntegralTypeArgumentNode arg ,
1288
- IntegerConstantInstruction constant , int k , Operand left , Operand right
1288
+ IntegerConstantInstruction constant , int k , Operand left , Operand right , int argval
1289
1289
|
1290
1290
// 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
1292
1293
left = constant .getAUse ( ) and
1293
- right = valueNumber ( paramNode .getInstruction ( ) ) .getAUse ( )
1294
+ right = valueNumber ( paramNode .getInstruction ( ) ) .getAUse ( ) and
1295
+ argval = arg .getValue ( )
1294
1296
|
1295
1297
// 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 ) |
1300
1299
// this block ensures that left = right + k, but it holds that `left != right + k`
1301
1300
areEqual = true and
1302
- constant .getValue ( ) .toInt ( ) != arg . getValue ( ) + k
1301
+ constant .getValue ( ) .toInt ( ) != argval + k
1303
1302
or
1304
1303
// this block ensures that or `left != right + k`, but it holds that `left = right + k`
1305
1304
areEqual = false and
1306
- constant .getValue ( ) .toInt ( ) = arg . getValue ( ) + k
1305
+ constant .getValue ( ) .toInt ( ) = argval + k
1307
1306
)
1308
1307
or
1309
1308
// 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 ) |
1314
1310
isLessThan = true and
1315
1311
// 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
1317
1313
or
1318
1314
// this block ensures that `left >= right + k`, but it holds that `left < right + k`
1319
1315
isLessThan = false and
1320
- constant .getValue ( ) .toInt ( ) < arg . getValue ( ) + k
1316
+ constant .getValue ( ) .toInt ( ) < argval + k
1321
1317
)
1322
1318
)
1323
1319
}
0 commit comments