Data flow: Simplify revFlowStore

This commit is contained in:
Tom Hvitved
2022-04-25 10:11:54 +02:00
parent cf0a1e748a
commit 2466288656
29 changed files with 29 additions and 29 deletions

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)

View File

@@ -782,7 +782,7 @@ private module Stage1 {
private predicate revFlowStore(Content c, NodeEx node, boolean toReturn, Configuration config) {
exists(NodeEx mid, TypedContent tc |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(_, c, pragma[only_bind_into](config)) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
store(node, tc, mid, _, config) and
c = tc.getContent()
)