Packaging a wand leads to having an inconsistent state causing unsoundness

[viper-admin]

Created by bitbucket user abdelzaher on 2018-05-22 20:51 Last updated on 2018-05-23 15:09

Here this example verifies as the package statement seems to lead us into some inconsistent state which should not be the case. While computing the footprint of the magic wand half permission is taken from LHS, and half is taken from current state which leads us with fact x.f == 2 && x.f == 3. So we are in an inconsistent state while proving the wand but this should not affect the global state. The two options that we have here are either rejecting the wand or verifying the wand after removing the permissions knowing that LHS can never be achieved.

#!scala

field f: Int

predicate p(x:Ref) {acc(x.f)}

method tst(x: Ref)
requires acc(x.f, 1/2) && x.f == 3
{
    package acc(x.f, 1/2) && x.f == 2 --* p(x)
    {
        fold p(x)
        assert x.f == 3
    }

    assert false
}

[viper-admin]

Bitbucket user abdelzaher on 2018-05-23 15:09:

• edited the description

[viper-admin]

@mschwerhoff commented on 2020-02-20 07:53

https://github.com/viperproject/silicon/issues/410 was marked as a duplicate of this issue.