@@ -4175,24 +4175,25 @@ private module Subpaths {
4175
4175
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
4176
4176
* `ret -> out` is summarized as the edge `arg -> out`.
4177
4177
*/
4178
- predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNodeMid out ) {
4179
- exists ( ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout |
4178
+ predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNode out ) {
4179
+ exists ( ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout , PathNodeMid out0 |
4180
4180
pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = par and
4181
- pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = out and
4181
+ pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = out0 and
4182
4182
subpaths03 ( arg , p , localStepToHidden * ( ret ) , o , sout , apout ) and
4183
4183
not ret .isHidden ( ) and
4184
4184
par .getNodeEx ( ) = p and
4185
- out .getNodeEx ( ) = o and
4186
- out .getState ( ) = sout and
4187
- out .getAp ( ) = apout
4185
+ out0 .getNodeEx ( ) = o and
4186
+ out0 .getState ( ) = sout and
4187
+ out0 .getAp ( ) = apout and
4188
+ ( out = out0 or out = out0 .projectToSink ( ) )
4188
4189
)
4189
4190
}
4190
4191
4191
4192
/**
4192
4193
* Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
4193
4194
*/
4194
4195
predicate retReach ( PathNode n ) {
4195
- exists ( PathNodeMid out | subpaths ( _, _, n , out ) | directReach ( out ) or retReach ( out ) )
4196
+ exists ( PathNode out | subpaths ( _, _, n , out ) | directReach ( out ) or retReach ( out ) )
4196
4197
or
4197
4198
exists ( PathNode mid |
4198
4199
retReach ( mid ) and
0 commit comments