Java: Implement clearsContent()

This commit is contained in:
Tom Hvitved
2020-06-22 20:28:04 +02:00
parent c057e82efa
commit c01f570d9e
3 changed files with 12 additions and 10 deletions

View File

@@ -195,6 +195,15 @@ predicate readStep(Node node1, Content f, Node node2) {
)
}
/**
* Holds if values stored inside content `c` are cleared at node `n`. For example,
* any value stored inside `f` is cleared at the pre-update node associated with `x`
* in `x.f = newValue`.
*/
predicate clearsContent(Node n, Content c) {
n = any(PostUpdateNode pun | storeStep(_, c, pun)).getPreUpdateNode()
}
/**
* Gets a representative (boxed) type for `t` for the purpose of pruning
* possible flow. A single type is used for all numeric types to account for