C++: Fix join-order problem in clearsContent

This commit is contained in:
Jeroen Ketema
2023-06-27 11:59:26 +02:00
parent 54632cd474
commit 2628552ef4

View File

@@ -786,7 +786,9 @@ predicate clearsContent(Node n, Content c) {
) )
or or
forex(PostUpdateNode pun, Content d | forex(PostUpdateNode pun, Content d |
d.impliesClearOf(c) and storeStepImpl(_, d, pun, true) and pun.getPreUpdateNode() = n pragma[only_bind_into](d).impliesClearOf(pragma[only_bind_into](c)) and
storeStepImpl(_, d, pun, true) and
pun.getPreUpdateNode() = n
| |
c.getIndirectionIndex() = d.getIndirectionIndex() c.getIndirectionIndex() = d.getIndirectionIndex()
) )