Choice of footprint of magic wand is inconsistent with ECOOP15 paper

[viper-admin]

Created by bitbucket user abdelzaher on 2018-05-22 20:34

Here in this example the permission acc(y.f) is transferred from the current state. In the case where x == y this will be inconsistent with the approach described in the paper as the permission should be transferred from the LHS of the wand.

The last assertion gives a verification error. It should verify because in case of x == y the permission in the footprint of the magic wand should be transferred from LHS of the wand leaving the permission in current state as it is.

#!scala

field f: Int

method foo(x: Ref, y: Ref) returns ()
requires acc(y.f) && y.f == 5
{
    package acc(x.f) && x.f == 3--* true
    {
        assert acc(y.f) && y.f == 5
    }

    if(x == y)
    {
        assert acc(y.f)
    }
}

[mschwerhoff]

This won't be easy to fix. An additional case-split might be a potential work-around, e.g. adding if (x == y) { assert false } to the body of the package statement.