@@ -460,7 +460,6 @@ module Impl<FullStateConfigSig Config> {
460460 * The Boolean `cc` records whether the node is reached through an
461461 * argument in a call.
462462 */
463- pragma [ assume_small_delta]
464463 private predicate fwdFlow ( NodeEx node , Cc cc ) {
465464 sourceNode ( node , _) and
466465 if hasSourceCallCtx ( ) then cc = true else cc = false
@@ -570,7 +569,6 @@ module Impl<FullStateConfigSig Config> {
570569 /**
571570 * Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
572571 */
573- pragma [ assume_small_delta]
574572 pragma [ nomagic]
575573 private predicate fwdFlowConsCand ( Content c ) {
576574 exists ( NodeEx mid , NodeEx node |
@@ -1216,7 +1214,6 @@ module Impl<FullStateConfigSig Config> {
12161214 fwdFlow1 ( _, _, _, _, _, _, t0 , t , ap , _) and t0 != t
12171215 }
12181216
1219- pragma [ assume_small_delta]
12201217 pragma [ nomagic]
12211218 private predicate fwdFlow0 (
12221219 NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
@@ -2777,7 +2774,6 @@ module Impl<FullStateConfigSig Config> {
27772774 /**
27782775 * Gets the number of `AccessPath`s that correspond to `apa`.
27792776 */
2780- pragma [ assume_small_delta]
27812777 private int countAps ( AccessPathApprox apa ) {
27822778 evalUnfold ( apa , false ) and
27832779 result = 1 and
@@ -2796,7 +2792,6 @@ module Impl<FullStateConfigSig Config> {
27962792 * that it is expanded to a precise head-tail representation.
27972793 */
27982794 language [ monotonicAggregates]
2799- pragma [ assume_small_delta]
28002795 private int countPotentialAps ( AccessPathApprox apa ) {
28012796 apa instanceof AccessPathApproxNil and result = 1
28022797 or
@@ -2833,7 +2828,6 @@ module Impl<FullStateConfigSig Config> {
28332828 }
28342829
28352830 private newtype TPathNode =
2836- pragma [ assume_small_delta]
28372831 TPathNodeMid (
28382832 NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t , AccessPath ap
28392833 ) {
@@ -2918,7 +2912,6 @@ module Impl<FullStateConfigSig Config> {
29182912
29192913 override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head_ ) }
29202914
2921- pragma [ assume_small_delta]
29222915 override AccessPathApproxCons getApprox ( ) {
29232916 result = TConsNil ( head_ , t ) and tail_ = TAccessPathNil ( )
29242917 or
@@ -2927,7 +2920,6 @@ module Impl<FullStateConfigSig Config> {
29272920 result = TCons1 ( head_ , this .length ( ) )
29282921 }
29292922
2930- pragma [ assume_small_delta]
29312923 override int length ( ) { result = 1 + tail_ .length ( ) }
29322924
29332925 private string toStringImpl ( boolean needsSuffix ) {
@@ -3379,7 +3371,6 @@ module Impl<FullStateConfigSig Config> {
33793371 * Holds if data may flow from `mid` to `node`. The last step in or out of
33803372 * a callable is recorded by `cc`.
33813373 */
3382- pragma [ assume_small_delta]
33833374 pragma [ nomagic]
33843375 private predicate pathStep0 (
33853376 PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t ,
@@ -3592,7 +3583,6 @@ module Impl<FullStateConfigSig Config> {
35923583 )
35933584 }
35943585
3595- pragma [ assume_small_delta]
35963586 pragma [ nomagic]
35973587 private predicate pathThroughCallable0 (
35983588 DataFlowCall call , PathNodeMid mid , ReturnKindExt kind , FlowState state , CallContext cc ,
0 commit comments