class Program {
var x: int;
method a(a: seq)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
assert rd(a[*].f);
call b(a);
}
method b(a: seq)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
assert rd(a[*].f);
}
method c(a: seq)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
call void(a[1]);
call void(a[0]);
}
method c1(a: seq) // ERROR: should fail to verify postcondition
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd(a[*].f);
{
call dispose(a[1]);
}
method d(a: seq)
requires |a| > 2;
requires rd(a[*].f);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd*(a[*].f);
{
call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
var x: int;
call x := some_number();
call dispose(a[x]); // slighly more interesting, but still clearly ok
}
method e(a: seq) // ERROR: should fail to verify postcondition
requires |a| > 2;
requires acc(a[*].f,10);
requires forall i in [0..|a|-1] :: a[i] != null;
requires a[0].f == 1;
ensures rd*(a[*].f);
{
var x: int;
call x := some_number();
call dispose2(a[x]);
}
method some_number() returns (a: int)
ensures 0 <= a && a < 3;
{
a := 1;
}
method dispose(a: A) requires rd(a.f); {}
method dispose2(a: A) requires acc(a.f,10); {}
method void(a: A) requires rd(a.f); ensures rd(a.f); {}
}
class A {
var f: int;
}