mirror of
https://github.com/github/codeql.git
synced 2025-12-23 12:16:33 +01:00
Address review comments
This commit is contained in:
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuratio
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
readSet(node1, cs, node2, config) and
|
readSet(node1, cs, node2, config) and
|
||||||
@@ -507,7 +507,7 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate clearsContentEx(NodeEx n, Content c) {
|
private predicate clearsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
clearsContentCached(n.asNode(), cs) and
|
clearsContentCached(n.asNode(), cs) and
|
||||||
@@ -516,7 +516,7 @@ private predicate clearsContentEx(NodeEx n, Content c) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// inline to reduce fan-out via `getAReadContent`
|
// inline to reduce fan-out via `getAReadContent`
|
||||||
pragma[inline]
|
bindingset[c]
|
||||||
private predicate expectsContentEx(NodeEx n, Content c) {
|
private predicate expectsContentEx(NodeEx n, Content c) {
|
||||||
exists(ContentSet cs |
|
exists(ContentSet cs |
|
||||||
expectsContentCached(n.asNode(), cs) and
|
expectsContentCached(n.asNode(), cs) and
|
||||||
|
|||||||
Reference in New Issue
Block a user