@@ -840,7 +840,10 @@ private predicate adjacentDefUseFlow(Node nodeFrom, Node nodeTo) {
840
840
)
841
841
}
842
842
843
- private module ReadNodeFlow {
843
+ /**
844
+ * INTERNAL: Do not use.
845
+ */
846
+ module ReadNodeFlow {
844
847
/** Holds if the read node `nodeTo` should receive flow from `nodeFrom`. */
845
848
predicate flowInto ( Node nodeFrom , ReadNode nodeTo ) {
846
849
nodeTo .isInitial ( ) and
@@ -860,7 +863,12 @@ private module ReadNodeFlow {
860
863
)
861
864
}
862
865
863
- /** Holds if the read node `nodeTo` should receive flow from the read node `nodeFrom`. */
866
+ /**
867
+ * Holds if the read node `nodeTo` should receive flow from the read node `nodeFrom`.
868
+ *
869
+ * This happens when `readFrom` is _not_ the source of a `readStep`, and `nodeTo` is
870
+ * the `ReadNode` that represents an address that directly depends on `nodeFrom`.
871
+ */
864
872
predicate flowThrough ( ReadNode nodeFrom , ReadNode nodeTo ) {
865
873
not readStep ( nodeFrom , _, _) and
866
874
nodeFrom .getOuter ( ) = nodeTo
@@ -908,11 +916,16 @@ module StoreNodeFlow {
908
916
nodeTo .flowInto ( Ssa:: getDestinationAddress ( instrFrom ) )
909
917
}
910
918
911
- /** Holds if the store node `nodeTo` should receive flow from `nodeFom`. */
912
- predicate flowThrough ( StoreNode nFrom , StoreNode nodeTo ) {
919
+ /**
920
+ * Holds if the store node `nodeTo` should receive flow from `nodeFom`.
921
+ *
922
+ * This happens when `nodeFrom` is _not_ the source of a `storeStep`, and `nodeFrom` is
923
+ * the `Storenode` that represents an address that directly depends on `nodeTo`.
924
+ */
925
+ predicate flowThrough ( StoreNode nodeFrom , StoreNode nodeTo ) {
913
926
// Flow through a post update node that doesn't need a store step.
914
- not storeStep ( nFrom , _, _) and
915
- nodeTo .getOuter ( ) = nFrom
927
+ not storeStep ( nodeFrom , _, _) and
928
+ nodeTo .getOuter ( ) = nodeFrom
916
929
}
917
930
918
931
/**
0 commit comments