Merged requested to merge simonfv/iris:persistent-points-to-2 into master
This is the same as !493 (closed) but based on !486 (merged). The overall description in !493 (closed) still applies.
As in the previous MR I've used the notation
l ↦□ v for the new persistent points-to predicate and changed the notation used by
gen_inv_heap. In the original MR description I argued for this choice and @jung replied with some additional arguments to consider. I think the conclusion is that using
l ↦□ v for the persistent points-to predicate is a good idea but that we need to come up with some other notation for
gen_inv_heap than what currently is in this MR.