Incorrect handling of method calls in package statements

[marcoeilers]

Old-expressions in postconditions of the called method are not handled correctly. For example, the following code does not verify:

field f: Int

method test(x: Ref) returns (r: Int)
  requires acc(x.f)
  ensures r == old(x.f)
{
  r := x.f
}

method foo(x: Ref) {
  package acc(x.f) --* true {
    var tmp: Int
    tmp := test(x) // Error here, caused by the *ensures*!
  }
}

Silicon reports a verification error when trying to evaluate old(x.f) in the method postcondition when producing it inside the package statement; it claims there is no permission to x.f, even though there obviously is.

[marcoeilers]

Fixed by PR #699.