0

How can I declare a method requiring a wildcard permission and returning exactly the same permission.

I would like the write something like this:

field fd:Int

method foo(p:Ref) returns (res:Int)
    requires acc(p.fd,wildcard)
    ensures acc(p.fd,old(perm(p.fd)))
    {
      res := p.fd
    }

But then I get an error.

Consistency error: Perm and forperm in this context are only allowed if nested under inhale-exhale assertions.
rsaill
  • 91
  • 1
  • 7

1 Answers1

0

Method pre- and postconditions must not contain perm()-expressions because the value of those expressions would be different when evaluated by a method caller: If a caller has a full permission, then old(perm(p.fd)) would evaluate to a full permission for the caller even though it would evaluate only to a wildcard amount for the callee.

To pass a wildcard permission amount and get the same amount back, you could give the method an additional perm-typed parameter, and then let callers choose an arbitrarily small permission amount:

field fd:Int

method foo(p:Ref, prm: Perm) returns (res:Int)
    requires prm > none
    requires acc(p.fd, prm)
    ensures acc(p.fd, prm)
    {
      res := p.fd
    }

method caller()
{
    var r: Ref
    r := new(fd)
    var res: Int
    res := foo(r, 1/10)
}
user3314215
  • 66
  • 1