[Alias Analysis] node materialization happens too late

[viper-admin]

Created by bitbucket user caterinaurban on 2016-09-06 14:17 Last updated on 2016-09-09 16:42

The may alias analysis has no information at the beginning of the program. As a consequence, the permission inference on the following program:

#!Scala
field f: Ref

method Foo(a: Ref, b: Ref)
{
    exhale acc(b.f)
    inhale acc(a.f)
    a.f := null
}

also infers the following precondition:

acc(a.f, write)

[viper-admin]

Bitbucket user caterinaurban on 2016-09-09 16:40:

• edited the description

[viper-admin]

Bitbucket user caterinaurban commented on 2016-09-09 16:42

I cannot reproduce the issue anymore.

[viper-admin]

Bitbucket user caterinaurban on 2016-09-09 16:42:

• changed state from new to closed