Package duplicate resources in magic wand leads to unsoundness

[viper-admin]

Created by bitbucket user BR_ on 2020-02-20 01:34
Last updated on 2020-02-20 07:53

The following code proves false:

field data: Int

method foo(x: Ref)
    requires acc(x.data)
{
    package acc(x.data) --* false {
        assert acc(x.data) && acc(x.data)
        assert false
    }

    assert acc(x.data)
    apply acc(x.data) --* false
    assert false
}

We are using the Silicon back-end, with the latest build.

‌

[viper-admin]

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

Reduced example, still unsound:

field data: Int

method foo(x: Ref)
    requires acc(x.data)
{
    package acc(x.data) --* false {
        assert acc(x.data) && acc(x.data)
        assert false
    }

    assert false
}

The underlying problem is that the inconsistent state that — expectedly — exists at the end of package “escapes” the packaging scope.

[viper-admin]

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

Duplicate of #338.

[viper-admin]

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

• changed state from new to duplicate