@@ -785,24 +785,26 @@ module TypeTracking<TypeTrackingInput I> {
785785 )
786786 }
787787
788+ private Node getNodeMid ( PathNodeFwd n ) { n = TPathNodeMid ( result , _) }
789+
790+ private Node getNodeSink ( PathNodeFwd n ) { n = TPathNodeSink ( result ) }
791+
788792 private predicate edgeCand ( PathNodeFwd n1 , PathNodeFwd n2 ) {
789793 exists ( PathNodeFwd tgt |
790- edgeCand ( n1 . getNode ( ) , n1 .getTypeTracker ( ) , tgt . getNode ( ) , tgt .getTypeTracker ( ) )
794+ edgeCand ( getNodeMid ( n1 ) , n1 .getTypeTracker ( ) , getNodeMid ( tgt ) , tgt .getTypeTracker ( ) )
791795 |
792796 n2 = tgt
793797 or
794- n2 = TPathNodeSink ( tgt . getNode ( ) ) and tgt .getTypeTracker ( ) .end ( )
798+ n2 = TPathNodeSink ( getNodeMid ( tgt ) ) and tgt .getTypeTracker ( ) .end ( )
795799 )
796800 or
797801 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 )
801804 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 ( )
806808 }
807809
808810 private predicate reachRev ( PathNodeFwd n ) {
0 commit comments