@@ -863,7 +863,12 @@ module ReadNodeFlow {
863
863
)
864
864
}
865
865
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
+ */
867
872
predicate flowThrough ( ReadNode nodeFrom , ReadNode nodeTo ) {
868
873
not readStep ( nodeFrom , _, _) and
869
874
nodeFrom .getOuter ( ) = nodeTo
@@ -911,11 +916,16 @@ module StoreNodeFlow {
911
916
nodeTo .flowInto ( Ssa:: getDestinationAddress ( instrFrom ) )
912
917
}
913
918
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 ) {
916
926
// 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
919
929
}
920
930
921
931
/**
0 commit comments