DataFlow: Sync identical files.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-01-27 16:24:31 +00:00
parent a691535e77
commit 95b15825f9
39 changed files with 195 additions and 39 deletions

View File

@@ -1487,6 +1487,10 @@ private module MkStage<StageSig PrevStage> {
PrevStage::readStepCand(node1, _, _, config)
}
bindingset[ap, c]
pragma[inline_late]
private predicate hasHeadContent(Ap ap, Content c) { getHeadContent(ap) = c }
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
@@ -1494,7 +1498,7 @@ private module MkStage<StageSig PrevStage> {
) {
fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
PrevStage::readStepCand(node1, c, node2, config) and
getHeadContent(ap) = c
hasHeadContent(ap, c)
}
pragma[nomagic]

View File

@@ -1487,6 +1487,10 @@ private module MkStage<StageSig PrevStage> {
PrevStage::readStepCand(node1, _, _, config)
}
bindingset[ap, c]
pragma[inline_late]
private predicate hasHeadContent(Ap ap, Content c) { getHeadContent(ap) = c }
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
@@ -1494,7 +1498,7 @@ private module MkStage<StageSig PrevStage> {
) {
fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
PrevStage::readStepCand(node1, c, node2, config) and
getHeadContent(ap) = c
hasHeadContent(ap, c)
}
pragma[nomagic]

View File

@@ -1487,6 +1487,10 @@ private module MkStage<StageSig PrevStage> {
PrevStage::readStepCand(node1, _, _, config)
}
bindingset[ap, c]
pragma[inline_late]
private predicate hasHeadContent(Ap ap, Content c) { getHeadContent(ap) = c }
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
@@ -1494,7 +1498,7 @@ private module MkStage<StageSig PrevStage> {
) {
fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
PrevStage::readStepCand(node1, c, node2, config) and
getHeadContent(ap) = c
hasHeadContent(ap, c)
}
pragma[nomagic]

View File

@@ -1487,6 +1487,10 @@ private module MkStage<StageSig PrevStage> {
PrevStage::readStepCand(node1, _, _, config)
}
bindingset[ap, c]
pragma[inline_late]
private predicate hasHeadContent(Ap ap, Content c) { getHeadContent(ap) = c }
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
@@ -1494,7 +1498,7 @@ private module MkStage<StageSig PrevStage> {
) {
fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
PrevStage::readStepCand(node1, c, node2, config) and
getHeadContent(ap) = c
hasHeadContent(ap, c)
}
pragma[nomagic]

View File

@@ -1487,6 +1487,10 @@ private module MkStage<StageSig PrevStage> {
PrevStage::readStepCand(node1, _, _, config)
}
bindingset[ap, c]
pragma[inline_late]
private predicate hasHeadContent(Ap ap, Content c) { getHeadContent(ap) = c }
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
@@ -1494,7 +1498,7 @@ private module MkStage<StageSig PrevStage> {
) {
fwdFlowRead0(node1, state, cc, summaryCtx, argAp, ap, config) and
PrevStage::readStepCand(node1, c, node2, config) and
getHeadContent(ap) = c
hasHeadContent(ap, c)
}
pragma[nomagic]