Use node variable in all disjuncts

This commit is contained in:
Jeroen Ketema
2022-03-15 10:18:04 +01:00
parent 9a0e94f389
commit 157a36bc4f
28 changed files with 28 additions and 56 deletions

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and

View File

@@ -381,8 +381,7 @@ private predicate fullBarrier(NodeEx node, Configuration config) {
pragma[nomagic]
private predicate stateBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and