Framing of locations within predicates is not retrospective

[viper-admin]

Created by @alexanderjsummers on 2018-10-13 12:19

In the following example, the assertions can't be proven. Adding copies of the assertions before the loop fixed the problem; the reason is that locations inside the predicate instances are only framed after they have been recorded as being inside (i.e. it is the unfolding of the predicates before the loop that makes the difference, not the particular assertions themselves).

#!scala
field f: Int

predicate P(self: Ref) { acc(self.f) }

method test(x: Ref, y: Ref)
    requires P(x) && P(y)
{
    var i: Int := 0;
    // assert (unfolding P(x) in x.f) == old(unfolding P(x) in x.f)
    // assert (unfolding P(y) in y.f) == old(unfolding P(y) in y.f)
    while (i < 10)
        invariant acc(P(x), 1/2) && acc(P(y), 1/2) && i <= 10
    {
        i := i + 1;
    }
    assert (unfolding P(x) in x.f) == old(unfolding P(x) in x.f)
    assert (unfolding P(y) in y.f) == old(unfolding P(y) in y.f)
} 

[tdardinier]

Similar issue as in #278 and #355, which is due to how Carbon handles exhale statements with known-folded permissions.