@@ -315,17 +315,17 @@ signature module ArgsAreInstantiationsOfInputSig {
315315 * If `i` is an inherent implementation, `tp` is a type parameter of the type being
316316 * implemented, otherwise `tp` is a type parameter of the trait (being implemented).
317317 *
318- * `pos ` is one of the positions in `f` in which the relevant type occours .
318+ * `posAdj ` is one of the positions in `f` in which the relevant type occurs .
319319 */
320- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
320+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ) ;
321321
322322 /** A call whose argument types are to be checked. */
323323 class Call {
324324 string toString ( ) ;
325325
326326 Location getLocation ( ) ;
327327
328- Type getArgType ( FunctionPosition pos , TypePath path ) ;
328+ Type getArgType ( FunctionPosition posAdj , TypePath path ) ;
329329
330330 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
331331 }
@@ -339,9 +339,9 @@ signature module ArgsAreInstantiationsOfInputSig {
339339module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
340340 pragma [ nomagic]
341341 private predicate toCheckRanked (
342- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
342+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj , int rnk
343343 ) {
344- Input:: toCheck ( i , f , tp , pos ) and
344+ Input:: toCheck ( i , f , tp , posAdj ) and
345345 tp =
346346 rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
347347 Input:: toCheck ( i , f , tp0 , _) and
@@ -353,41 +353,45 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
353353
354354 pragma [ nomagic]
355355 private predicate toCheck (
356- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
356+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ,
357+ AssocFunctionType t
357358 ) {
358- Input:: toCheck ( i , f , tp , pos ) and
359- t .appliesTo ( f , i , pos )
359+ exists ( FunctionPosition pos |
360+ Input:: toCheck ( i , f , tp , posAdj ) and
361+ t .appliesTo ( f , i , pos ) and
362+ posAdj = pos .getFunctionCallAdjusted ( f )
363+ )
360364 }
361365
362366 private newtype TCallAndPos =
363- MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
367+ MkCallAndPos ( Input:: Call call , FunctionPosition posAdj ) { exists ( call .getArgType ( posAdj , _) ) }
364368
365369 /** A call tagged with a position. */
366370 private class CallAndPos extends MkCallAndPos {
367371 Input:: Call call ;
368- FunctionPosition pos ;
372+ FunctionPosition posAdj ;
369373
370- CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
374+ CallAndPos ( ) { this = MkCallAndPos ( call , posAdj ) }
371375
372376 Input:: Call getCall ( ) { result = call }
373377
374- FunctionPosition getPos ( ) { result = pos }
378+ FunctionPosition getPosAdj ( ) { result = posAdj }
375379
376380 Location getLocation ( ) { result = call .getLocation ( ) }
377381
378- Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
382+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( posAdj , path ) }
379383
380- string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
384+ string toString ( ) { result = call .toString ( ) + " [arg " + posAdj + "]" }
381385 }
382386
383387 pragma [ nomagic]
384388 private predicate potentialInstantiationOf0 (
385- CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
389+ CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition posAdj , Function f ,
386390 TypeAbstraction abs , AssocFunctionType constraint
387391 ) {
388- cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
392+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( posAdj ) ) and
389393 call .hasTargetCand ( abs , f ) and
390- toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
394+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( posAdj ) , constraint )
391395 }
392396
393397 private module ArgIsInstantiationOfToIndexInput implements
@@ -397,9 +401,9 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
397401 predicate potentialInstantiationOf (
398402 CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
399403 ) {
400- exists ( Input:: Call call , TypeParameter tp , FunctionPosition pos , int rnk , Function f |
401- potentialInstantiationOf0 ( cp , call , tp , pos , f , abs , constraint ) and
402- toCheckRanked ( abs , f , tp , pos , rnk )
404+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition posAdj , int rnk , Function f |
405+ potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
406+ toCheckRanked ( abs , f , tp , posAdj , rnk )
403407 |
404408 rnk = 0
405409 or
@@ -415,20 +419,21 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
415419
416420 pragma [ nomagic]
417421 private predicate argIsInstantiationOf (
418- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i , Function f , int rnk
422+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
419423 ) {
420- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
421- toCheckRanked ( i , f , _, pos , rnk )
424+ exists ( FunctionPosition posAdj |
425+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , posAdj ) , i , _) and
426+ toCheckRanked ( i , f , _, posAdj , rnk )
427+ )
422428 }
423429
424430 pragma [ nomagic]
425431 private predicate argsAreInstantiationsOfToIndex (
426432 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
427433 ) {
428- exists ( FunctionPosition pos |
429- argIsInstantiationOf ( call , pos , i , f , rnk ) and
430- call .hasTargetCand ( i , f )
431- |
434+ argIsInstantiationOf ( call , i , f , rnk ) and
435+ call .hasTargetCand ( i , f ) and
436+ (
432437 rnk = 0
433438 or
434439 argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
@@ -467,9 +472,9 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
467472
468473 pragma [ nomagic]
469474 private predicate argsAreNotInstantiationsOf0 (
470- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
475+ Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
471476 ) {
472- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
477+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , posAdj ) , i , _, _)
473478 }
474479
475480 /**
@@ -480,10 +485,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
480485 */
481486 pragma [ nomagic]
482487 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
483- exists ( FunctionPosition pos |
484- argsAreNotInstantiationsOf0 ( call , pos , i ) and
488+ exists ( FunctionPosition posAdj |
489+ argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
485490 call .hasTargetCand ( i , f ) and
486- Input:: toCheck ( i , f , _, pos )
491+ Input:: toCheck ( i , f , _, posAdj )
487492 )
488493 }
489494}
0 commit comments