@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
2629
2629
/**
2630
2630
* Gets the number of `AccessPath`s that correspond to `apa`.
2631
2631
*/
2632
+ pragma [ assume_small_delta]
2632
2633
private int countAps ( AccessPathApprox apa , Configuration config ) {
2633
2634
evalUnfold ( apa , false , config ) and
2634
2635
result = 1 and
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
2647
2648
* that it is expanded to a precise head-tail representation.
2648
2649
*/
2649
2650
language [ monotonicAggregates]
2651
+ pragma [ assume_small_delta]
2650
2652
private int countPotentialAps ( AccessPathApprox apa , Configuration config ) {
2651
2653
apa instanceof AccessPathApproxNil and result = 1
2652
2654
or
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
2681
2683
}
2682
2684
2683
2685
private newtype TPathNode =
2686
+ pragma [ assume_small_delta]
2684
2687
TPathNodeMid (
2685
2688
NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap , Configuration config
2686
2689
) {
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
2778
2781
2779
2782
override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head ) }
2780
2783
2784
+ pragma [ assume_small_delta]
2781
2785
override AccessPathApproxCons getApprox ( ) {
2782
2786
result = TConsNil ( head , tail .( AccessPathNil ) .getType ( ) )
2783
2787
or
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
2786
2790
result = TCons1 ( head , this .length ( ) )
2787
2791
}
2788
2792
2793
+ pragma [ assume_small_delta]
2789
2794
override int length ( ) { result = 1 + tail .length ( ) }
2790
2795
2791
2796
private string toStringImpl ( boolean needsSuffix ) {
@@ -3155,6 +3160,7 @@ private predicate pathNode(
3155
3160
* Holds if data may flow from `mid` to `node`. The last step in or out of
3156
3161
* a callable is recorded by `cc`.
3157
3162
*/
3163
+ pragma [ assume_small_delta]
3158
3164
pragma [ nomagic]
3159
3165
private predicate pathStep (
3160
3166
PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap
0 commit comments