@@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration
26292629/**
26302630 * Gets the number of `AccessPath`s that correspond to `apa`.
26312631 */
2632+ pragma [ assume_small_delta]
26322633private int countAps ( AccessPathApprox apa , Configuration config ) {
26332634 evalUnfold ( apa , false , config ) and
26342635 result = 1 and
@@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) {
26472648 * that it is expanded to a precise head-tail representation.
26482649 */
26492650language [ monotonicAggregates]
2651+ pragma [ assume_small_delta]
26502652private int countPotentialAps ( AccessPathApprox apa , Configuration config ) {
26512653 apa instanceof AccessPathApproxNil and result = 1
26522654 or
@@ -2681,6 +2683,7 @@ private newtype TAccessPath =
26812683 }
26822684
26832685private newtype TPathNode =
2686+ pragma [ assume_small_delta]
26842687 TPathNodeMid (
26852688 NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap , Configuration config
26862689 ) {
@@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
27782781
27792782 override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head ) }
27802783
2784+ pragma [ assume_small_delta]
27812785 override AccessPathApproxCons getApprox ( ) {
27822786 result = TConsNil ( head , tail .( AccessPathNil ) .getType ( ) )
27832787 or
@@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons {
27862790 result = TCons1 ( head , this .length ( ) )
27872791 }
27882792
2793+ pragma [ assume_small_delta]
27892794 override int length ( ) { result = 1 + tail .length ( ) }
27902795
27912796 private string toStringImpl ( boolean needsSuffix ) {
@@ -3155,6 +3160,7 @@ private predicate pathNode(
31553160 * Holds if data may flow from `mid` to `node`. The last step in or out of
31563161 * a callable is recorded by `cc`.
31573162 */
3163+ pragma [ assume_small_delta]
31583164pragma [ nomagic]
31593165private predicate pathStep (
31603166 PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap
0 commit comments