@@ -4300,22 +4300,26 @@ private module Subpaths {
4300
4300
)
4301
4301
}
4302
4302
4303
+ pragma [ nomagic]
4304
+ private predicate hasSuccessor ( PathNode pred , PathNodeMid succ , NodeEx succNode ) {
4305
+ succ = pred .getASuccessor ( ) and
4306
+ succNode = succ .getNodeEx ( )
4307
+ }
4308
+
4303
4309
/**
4304
4310
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
4305
4311
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
4306
4312
* `ret -> out` is summarized as the edge `arg -> out`.
4307
4313
*/
4308
4314
predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNode out ) {
4309
4315
exists ( ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout , PathNodeMid out0 |
4310
- pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = pragma [ only_bind_into ] ( par ) and
4311
- pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = out0 and
4316
+ pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = pragma [ only_bind_into ] ( out0 ) and
4312
4317
subpaths03 ( pragma [ only_bind_into ] ( arg ) , p , localStepToHidden * ( ret ) , o , sout , apout ) and
4318
+ hasSuccessor ( pragma [ only_bind_into ] ( arg ) , par , p ) and
4313
4319
not ret .isHidden ( ) and
4314
- par .getNodeEx ( ) = p and
4315
- out0 .getNodeEx ( ) = o and
4316
- out0 .getState ( ) = sout and
4317
- out0 .getAp ( ) = apout and
4318
- ( out = out0 or out = out0 .projectToSink ( ) )
4320
+ pathNode ( out0 , o , sout , _, _, apout , _, _)
4321
+ |
4322
+ out = out0 or out = out0 .projectToSink ( )
4319
4323
)
4320
4324
}
4321
4325
0 commit comments