@@ -785,24 +785,26 @@ module TypeTracking<TypeTrackingInput I> {
785
785
)
786
786
}
787
787
788
+ private Node getNodeMid ( PathNodeFwd n ) { n = TPathNodeMid ( result , _) }
789
+
790
+ private Node getNodeSink ( PathNodeFwd n ) { n = TPathNodeSink ( result ) }
791
+
788
792
private predicate edgeCand ( PathNodeFwd n1 , PathNodeFwd n2 ) {
789
793
exists ( PathNodeFwd tgt |
790
- edgeCand ( n1 . getNode ( ) , n1 .getTypeTracker ( ) , tgt . getNode ( ) , tgt .getTypeTracker ( ) )
794
+ edgeCand ( getNodeMid ( n1 ) , n1 .getTypeTracker ( ) , getNodeMid ( tgt ) , tgt .getTypeTracker ( ) )
791
795
|
792
796
n2 = tgt
793
797
or
794
- n2 = TPathNodeSink ( tgt . getNode ( ) ) and tgt .getTypeTracker ( ) .end ( )
798
+ n2 = TPathNodeSink ( getNodeMid ( tgt ) ) and tgt .getTypeTracker ( ) .end ( )
795
799
)
796
800
or
797
801
n1 .getTypeTracker ( ) .end ( ) and
798
- flowsTo ( n1 .getNode ( ) , n2 .getNode ( ) ) and
799
- n1 .getNode ( ) != n2 .getNode ( ) and
800
- n2 instanceof TPathNodeSink
802
+ flowsTo ( getNodeMid ( n1 ) , getNodeSink ( n2 ) ) and
803
+ getNodeMid ( n1 ) != getNodeSink ( n2 )
801
804
or
802
- sourceSimpleLocalSmallSteps ( n1 .getNode ( ) , n2 .getNode ( ) ) and
803
- n1 .getNode ( ) != n2 .getNode ( ) and
804
- n1 .isSource ( ) and
805
- n2 .isSink ( )
805
+ sourceSimpleLocalSmallSteps ( n1 .getNode ( ) , getNodeSink ( n2 ) ) and
806
+ n1 .getNode ( ) != getNodeSink ( n2 ) and
807
+ n1 .isSource ( )
806
808
}
807
809
808
810
private predicate reachRev ( PathNodeFwd n ) {
0 commit comments