@@ -4206,10 +4206,11 @@ private module Subpaths {
4206
4206
pragma [ nomagic]
4207
4207
private predicate subpaths01 (
4208
4208
PathNodeImpl arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
4209
- NodeEx out , FlowState sout , AccessPath apout
4209
+ NodeEx out , FlowState sout , CallContext ccout , AccessPath apout
4210
4210
) {
4211
4211
exists ( Configuration config |
4212
- pathThroughCallable ( arg , out , pragma [ only_bind_into ] ( sout ) , _, pragma [ only_bind_into ] ( apout ) ) and
4212
+ pathThroughCallable ( arg , out , pragma [ only_bind_into ] ( sout ) , ccout ,
4213
+ pragma [ only_bind_into ] ( apout ) ) and
4213
4214
pathIntoCallable ( arg , par , _, _, innercc , sc , _, config ) and
4214
4215
paramFlowsThrough ( kind , pragma [ only_bind_into ] ( sout ) , innercc , sc ,
4215
4216
pragma [ only_bind_into ] ( apout ) , _, unbindConf ( config ) ) and
@@ -4224,10 +4225,11 @@ private module Subpaths {
4224
4225
pragma [ nomagic]
4225
4226
private predicate subpaths02 (
4226
4227
PathNode arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
4227
- NodeEx out , FlowState sout , AccessPath apout
4228
+ NodeEx out , FlowState sout , CallContext ccout , AccessPath apout , Configuration config
4228
4229
) {
4229
- subpaths01 ( arg , par , sc , innercc , kind , out , sout , apout ) and
4230
- out .asNode ( ) = kind .getAnOutNode ( _)
4230
+ subpaths01 ( arg , par , sc , innercc , kind , out , sout , ccout , apout ) and
4231
+ out .asNode ( ) = kind .getAnOutNode ( _) and
4232
+ config = getPathNodeConf ( arg )
4231
4233
}
4232
4234
4233
4235
pragma [ nomagic]
@@ -4238,12 +4240,14 @@ private module Subpaths {
4238
4240
*/
4239
4241
pragma [ nomagic]
4240
4242
private predicate subpaths03 (
4241
- PathNode arg , ParamNodeEx par , PathNodeMid ret , NodeEx out , FlowState sout , AccessPath apout
4243
+ PathNodeMid arg , ParamNodeEx par , PathNodeMid ret , NodeEx out , FlowState sout ,
4244
+ CallContext ccout , AccessPath apout , SummaryCtx scout , Configuration config
4242
4245
) {
4243
4246
exists ( SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind , RetNodeEx retnode |
4244
- subpaths02 ( arg , par , sc , innercc , kind , out , sout , apout ) and
4245
- pathNode ( ret , retnode , sout , innercc , sc , apout , unbindConf ( getPathNodeConf ( arg ) ) , _) and
4246
- kind = retnode .getKind ( )
4247
+ subpaths02 ( arg , par , sc , innercc , kind , out , sout , ccout , apout , config ) and
4248
+ pathNode ( ret , retnode , sout , innercc , sc , apout , config , _) and
4249
+ kind = retnode .getKind ( ) and
4250
+ scout = arg .getSummaryCtx ( )
4247
4251
)
4248
4252
}
4249
4253
@@ -4263,16 +4267,17 @@ private module Subpaths {
4263
4267
* `ret -> out` is summarized as the edge `arg -> out`.
4264
4268
*/
4265
4269
predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNode out ) {
4266
- exists ( ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout , PathNodeMid out0 |
4270
+ exists (
4271
+ ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout , CallContext ccout ,
4272
+ SummaryCtx scout , PathNodeMid out0 , Configuration config
4273
+ |
4267
4274
pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = par and
4268
- pragma [ only_bind_into ] ( arg ) . getASuccessor ( ) = out0 and
4269
- subpaths03 ( arg , p , localStepToHidden * ( ret ) , o , sout , apout ) and
4275
+ subpaths03 ( arg , p , localStepToHidden * ( ret ) , o , sout , ccout , apout , scout , config ) and
4276
+ pathNode ( out0 , o , sout , ccout , scout , apout , config , _ ) and
4270
4277
not ret .isHidden ( ) and
4271
- par .getNodeEx ( ) = p and
4272
- out0 .getNodeEx ( ) = o and
4273
- out0 .getState ( ) = sout and
4274
- out0 .getAp ( ) = apout and
4275
- ( out = out0 or out = out0 .projectToSink ( ) )
4278
+ par .getNodeEx ( ) = p
4279
+ |
4280
+ out = out0 or out = out0 .projectToSink ( )
4276
4281
)
4277
4282
}
4278
4283
0 commit comments