Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -335,14 +335,19 @@ module Track<TrackInputSig Input> {
}
}

pragma[nomagic]
private predicate derivedStoreReadStep0(NamespaceNode namespace, string name, NameBindingNode node2) {
readStep(namespace.ref(), pragma[only_bind_into](name), node2)
}

/**
* Holds if `node1 -> node2` is derived by combining a store and a read step, with zero or more value steps and inheritance steps in-between.
*/
pragma[nomagic]
private predicate derivedStoreReadStep(NameBindingNode node1, NameBindingNode node2) {
exists(NamespaceNode namespace, string name |
node1 = namespace.getMember(pragma[only_bind_into](name)) and // getMember() combines a store step with subsequent inheritance steps
readStep(namespace.ref(), pragma[only_bind_into](name), node2) and
node1 = namespace.getMember(name) and // getMember() combines a store step with subsequent inheritance steps
derivedStoreReadStep0(namespace, name, node2) and
node1 != node2
)
}
Expand Down
Loading