@@ -863,7 +863,12 @@ module ReadNodeFlow {
863863 )
864864 }
865865
866- /** 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+ */
867872 predicate flowThrough ( ReadNode nodeFrom , ReadNode nodeTo ) {
868873 not readStep ( nodeFrom , _, _) and
869874 nodeFrom .getOuter ( ) = nodeTo
@@ -911,11 +916,16 @@ module StoreNodeFlow {
911916 nodeTo .flowInto ( Ssa:: getDestinationAddress ( instrFrom ) )
912917 }
913918
914- /** Holds if the store node `nodeTo` should receive flow from `nodeFom`. */
915- 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 ) {
916926 // Flow through a post update node that doesn't need a store step.
917- not storeStep ( nFrom , _, _) and
918- nodeTo .getOuter ( ) = nFrom
927+ not storeStep ( nodeFrom , _, _) and
928+ nodeTo .getOuter ( ) = nodeFrom
919929 }
920930
921931 /**
0 commit comments