[Silver Permission Inference] Weird results for some existing specifications.

[viper-admin]

Created by @dohrau on 2016-11-01 09:35

Consider the following example.

#!scala
field f: Ref

method foo(a: Ref, read: Perm)
    requires read > none
    requires acc(a.f.f, read)
{}

method bar(a: Ref)
    requires acc(a.f.f) && acc(a.f)
{}

Currently the permission inference produces the output below.

#!scala

field f: Ref

method foo(a: Ref, read: Perm)
  requires read > none
  requires acc(a.f, read)
  requires acc(a.f.f, read)
  requires read > none
{
}

method bar(a: Ref, read: Perm)
  requires read > none
  requires acc(a.f, read)
  requires acc(a.f, write)
  requires acc(a.f.f, write)
{
}

There are the following two issues:

• The permission inference splits an existing specification into two parts: One part contains all the permission related stuff and the other part contains the rest which is ignored. Currently, the condition read > none is in the part that gets ignored. As a result, the inference just adds another read > none to the precondition.

• The expression acc(a.f.f) && acc(a.f) is not self-framing and therefore either requires another read permission for a.f or requires the two permission predicates to be reordered. Currently, the permission inference does something in between: First the additional read permission is inferred and in the very end all permission predicates are sorted according to the length of their access paths.

[viper-admin]

@dohrau on 2016-11-01 09:35:

• edited the description