Update DataFlowImpl.qll copies

This commit is contained in:
Asger F
2023-09-25 10:05:29 +02:00
parent cfed7e9b6c
commit d501856519
29 changed files with 116 additions and 0 deletions

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)

View File

@@ -297,6 +297,10 @@ private module Config implements FullStateConfigSig {
predicate isBarrierOut(Node node) { any(Configuration config).isBarrierOut(node) }
predicate isBarrierIn(Node node, FlowState state) { none() }
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, Node node2) {
singleConfiguration() and
any(Configuration config).isAdditionalFlowStep(node1, node2)