@@ -2759,10 +2759,10 @@ module Impl<FullStateConfigSig Config> {
2759
2759
)
2760
2760
}
2761
2761
2762
- private AccessPathApprox getATail ( AccessPathApprox apa ) {
2763
- exists ( TypedContent head , DataFlowType t |
2764
- apa .isCons ( head , t , result ) and
2765
- Stage5:: consCand ( head , t , result )
2762
+ private predicate hasTail ( AccessPathApprox apa , DataFlowType t , AccessPathApprox tail ) {
2763
+ exists ( TypedContent head |
2764
+ apa .isCons ( head , t , tail ) and
2765
+ Stage5:: consCand ( head , t , tail )
2766
2766
)
2767
2767
}
2768
2768
@@ -2808,7 +2808,7 @@ module Impl<FullStateConfigSig Config> {
2808
2808
private int countPotentialAps ( AccessPathApprox apa ) {
2809
2809
apa instanceof AccessPathApproxNil and result = 1
2810
2810
or
2811
- result = strictsum ( AccessPathApprox tail | tail = getATail ( apa ) | countAps ( tail ) )
2811
+ result = strictsum ( DataFlowType t , AccessPathApprox tail | hasTail ( apa , t , tail ) | countAps ( tail ) )
2812
2812
}
2813
2813
2814
2814
private newtype TAccessPath =
@@ -2817,16 +2817,17 @@ module Impl<FullStateConfigSig Config> {
2817
2817
exists ( AccessPathApproxCons apa |
2818
2818
not evalUnfold ( apa , false ) and
2819
2819
head = apa .getHead ( ) and
2820
- tail .getApprox ( ) = getATail ( apa )
2820
+ hasTail ( apa , _ , tail .getApprox ( ) )
2821
2821
)
2822
2822
} or
2823
2823
TAccessPathCons2 ( TypedContent head1 , TypedContent head2 , int len ) {
2824
- exists ( AccessPathApproxCons apa |
2824
+ exists ( AccessPathApproxCons apa , AccessPathApprox tail |
2825
2825
evalUnfold ( apa , false ) and
2826
2826
not expensiveLen1to2unfolding ( apa ) and
2827
2827
apa .len ( ) = len and
2828
+ hasTail ( apa , _, tail ) and
2828
2829
head1 = apa .getHead ( ) and
2829
- head2 = getATail ( apa ) .getHead ( )
2830
+ head2 = tail .getHead ( )
2830
2831
)
2831
2832
} or
2832
2833
TAccessPathCons1 ( TypedContent head , int len ) {
0 commit comments