@@ -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,18 +419,18 @@ 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 , FunctionPosition posAdj , ImplOrTraitItemNode i , Function f , int rnk
419423 ) {
420- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
421- toCheckRanked ( i , f , _, pos , rnk )
424+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , posAdj ) , i , _) and
425+ toCheckRanked ( i , f , _, posAdj , rnk )
422426 }
423427
424428 pragma [ nomagic]
425429 private predicate argsAreInstantiationsOfToIndex (
426430 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
427431 ) {
428- exists ( FunctionPosition pos |
429- argIsInstantiationOf ( call , pos , i , f , rnk ) and
432+ exists ( FunctionPosition posAdj |
433+ argIsInstantiationOf ( call , posAdj , i , f , rnk ) and
430434 call .hasTargetCand ( i , f )
431435 |
432436 rnk = 0
@@ -467,9 +471,9 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
467471
468472 pragma [ nomagic]
469473 private predicate argsAreNotInstantiationsOf0 (
470- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
474+ Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
471475 ) {
472- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
476+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , posAdj ) , i , _, _)
473477 }
474478
475479 /**
@@ -480,10 +484,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
480484 */
481485 pragma [ nomagic]
482486 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
483- exists ( FunctionPosition pos |
484- argsAreNotInstantiationsOf0 ( call , pos , i ) and
487+ exists ( FunctionPosition posAdj |
488+ argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
485489 call .hasTargetCand ( i , f ) and
486- Input:: toCheck ( i , f , _, pos )
490+ Input:: toCheck ( i , f , _, posAdj )
487491 )
488492 }
489493}
0 commit comments