@@ -340,94 +340,13 @@ module ProductFlow {
340340 fwdIsSuccessor ( _, _, node1 , node2 )
341341 }
342342
343- pragma [ assume_small_delta]
344- pragma [ nomagic]
345- private predicate fwdLocalPathStep1 ( Flow1:: PathNode n ) {
346- fwdReachableInterprocEntry ( n , _)
347- or
348- exists ( Flow1:: PathNode mid |
349- fwdLocalPathStep1 ( mid ) and
350- localPathStep1 ( mid , n )
351- )
352- }
353-
354- pragma [ assume_small_delta]
355- pragma [ nomagic]
356- private predicate revLocalPathStep1 ( Flow1:: PathNode n ) {
357- fwdLocalPathStep1 ( n ) and
358- (
359- isSinkPair ( n , _)
360- or
361- interprocEdgePair ( n , _, _, _)
362- or
363- exists ( Flow1:: PathNode mid |
364- revLocalPathStep1 ( mid ) and
365- localPathStep1 ( n , mid )
366- )
367- )
368- }
369-
370- pragma [ assume_small_delta]
371- private predicate prunedLocalPathStep1 ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) {
372- revLocalPathStep1 ( n1 ) and
373- revLocalPathStep1 ( n2 ) and
374- localPathStep1 ( n1 , n2 )
375- }
376-
377- pragma [ nomagic]
378- private predicate fwdLocalPathStep2 ( Flow2:: PathNode n ) {
379- fwdReachableInterprocEntry ( _, n )
380- or
381- exists ( Flow2:: PathNode mid |
382- fwdLocalPathStep2 ( mid ) and
383- localPathStep2 ( mid , n )
384- )
385- }
386-
387- pragma [ assume_small_delta]
388- pragma [ nomagic]
389- private predicate revLocalPathStep2 ( Flow2:: PathNode n ) {
390- fwdLocalPathStep2 ( n ) and
391- (
392- isSinkPair ( _, n )
393- or
394- interprocEdgePair ( _, n , _, _)
395- or
396- exists ( Flow2:: PathNode mid |
397- revLocalPathStep2 ( mid ) and
398- localPathStep2 ( n , mid )
399- )
400- )
401- }
402-
403- pragma [ assume_small_delta]
404- private predicate prunedLocalPathStep2 ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) {
405- revLocalPathStep2 ( n1 ) and
406- revLocalPathStep2 ( n2 ) and
407- localPathStep2 ( n1 , n2 )
408- }
409-
410- private predicate localPathStep1SuccPlus ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) =
411- fastTC( prunedLocalPathStep1 / 2 ) ( n1 , n2 )
412-
413- private predicate localPathStep2SuccPlus ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) =
414- fastTC( prunedLocalPathStep2 / 2 ) ( n1 , n2 )
415-
416- private predicate localPathStep1Tc ( Flow1:: PathNode n1 , Flow1:: PathNode n2 ) {
417- localPathStep1SuccPlus ( n1 , n2 ) or n1 = n2
418- }
419-
420- private predicate localPathStep2Tc ( Flow2:: PathNode n1 , Flow2:: PathNode n2 ) {
421- localPathStep2SuccPlus ( n1 , n2 ) or n1 = n2
422- }
423-
424343 private predicate fwdIsSuccessor (
425344 Flow1:: PathNode pred1 , Flow2:: PathNode pred2 , Flow1:: PathNode succ1 , Flow2:: PathNode succ2
426345 ) {
427346 fwdReachableInterprocEntry ( pred1 , pred2 ) and
428347 exists ( Flow1:: PathNode mid1 , Flow2:: PathNode mid2 |
429- localPathStep1Tc ( pred1 , mid1 ) and
430- localPathStep2Tc ( pred2 , mid2 )
348+ localPathStep1 * ( pred1 , mid1 ) and
349+ localPathStep2 * ( pred2 , mid2 )
431350 |
432351 isSinkPair ( mid1 , mid2 ) and
433352 succ1 = mid1 and
0 commit comments