@@ -840,7 +840,10 @@ private predicate adjacentDefUseFlow(Node nodeFrom, Node nodeTo) {
840840 )
841841}
842842
843- private module ReadNodeFlow {
843+ /**
844+ * INTERNAL: Do not use.
845+ */
846+ module ReadNodeFlow {
844847 /** Holds if the read node `nodeTo` should receive flow from `nodeFrom`. */
845848 predicate flowInto ( Node nodeFrom , ReadNode nodeTo ) {
846849 nodeTo .isInitial ( ) and
@@ -860,7 +863,12 @@ private module ReadNodeFlow {
860863 )
861864 }
862865
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+ */
864872 predicate flowThrough ( ReadNode nodeFrom , ReadNode nodeTo ) {
865873 not readStep ( nodeFrom , _, _) and
866874 nodeFrom .getOuter ( ) = nodeTo
@@ -908,11 +916,16 @@ module StoreNodeFlow {
908916 nodeTo .flowInto ( Ssa:: getDestinationAddress ( instrFrom ) )
909917 }
910918
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 ) {
913926 // 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
916929 }
917930
918931 /**
0 commit comments