Shared: Address review comments.

This commit is contained in:
Michael Nebel
2024-08-26 15:24:22 +02:00
parent 4381bae5d1
commit 77bfe39ca7

View File

@@ -455,18 +455,15 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
)
}
pragma[nomagic]
private predicate nodeAndState(Flow::PathNode n, Node node, State state) {
n.getNode() = node and n.getState() = state
}
pragma[nomagic]
private predicate succNodeAndState(
Flow::PathNode pre, Node preNode, State preState, Flow::PathNode succ, Node succNode,
State succState
) {
nodeAndState(pre, preNode, preState) and
nodeAndState(succ, succNode, succState) and
pre.getNode() = preNode and
pre.getState() = preState and
succ.getNode() = succNode and
succ.getState() = succState and
pre.getASuccessor() = succ
}