@@ -140,10 +140,8 @@ private module LambdaFlow {
140140 }
141141
142142 pragma [ nomagic]
143- private TReturnPositionSimple viableReturnPosLambda (
144- DataFlowCall call , DataFlowCallOption lastCall , ReturnKind kind
145- ) {
146- result = TReturnPositionSimple0 ( viableCallableLambda ( call , lastCall ) , kind )
143+ private TReturnPositionSimple viableReturnPosLambda ( DataFlowCall call , ReturnKind kind ) {
144+ result = TReturnPositionSimple0 ( viableCallableLambda ( call , _) , kind )
147145 }
148146
149147 private predicate viableReturnPosOutNonLambda (
@@ -155,11 +153,12 @@ private module LambdaFlow {
155153 )
156154 }
157155
156+ pragma [ nomagic]
158157 private predicate viableReturnPosOutLambda (
159- DataFlowCall call , DataFlowCallOption lastCall , TReturnPositionSimple pos , OutNode out
158+ DataFlowCall call , TReturnPositionSimple pos , OutNode out
160159 ) {
161160 exists ( ReturnKind kind |
162- pos = viableReturnPosLambda ( call , lastCall , kind ) and
161+ pos = viableReturnPosLambda ( call , kind ) and
163162 out = getAnOutNode ( call , kind )
164163 )
165164 }
@@ -188,6 +187,7 @@ private module LambdaFlow {
188187 else any ( )
189188 }
190189
190+ pragma [ assume_small_delta]
191191 pragma [ nomagic]
192192 predicate revLambdaFlow0 (
193193 DataFlowCall lambdaCall , LambdaCallKind kind , Node node , DataFlowType t , boolean toReturn ,
@@ -274,6 +274,7 @@ private module LambdaFlow {
274274 )
275275 }
276276
277+ pragma [ assume_small_delta]
277278 pragma [ nomagic]
278279 predicate revLambdaFlowOut (
279280 DataFlowCall lambdaCall , LambdaCallKind kind , TReturnPositionSimple pos , DataFlowType t ,
@@ -285,7 +286,7 @@ private module LambdaFlow {
285286 or
286287 // non-linear recursion
287288 revLambdaFlowOutLambdaCall ( lambdaCall , kind , out , t , toJump , call , lastCall ) and
288- viableReturnPosOutLambda ( call , _ , pos , out )
289+ viableReturnPosOutLambda ( call , pos , out )
289290 )
290291 }
291292
0 commit comments