Chalice/tests/permission-model/channels.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

class C {
  var f: int;
  
  method t1(ch: C1)
    requires ch != null && rd(f);
    ensures true;
  {
    send ch(this) // ERROR
  }
  
  method t2(ch: C1)
    requires ch != null && acc(f);
    ensures true;
  {
    send ch(this)
  }
  
  method t3(ch: C2)
    requires ch != null && rd(f);
    ensures rd(f);
  {
    send ch(this)
    // ERROR: should fail to verify postcondition
  }
  
  method t4(ch: C1, a: C) returns (b: C)
    requires ch != null && credit(ch, 1) && rd(ch.mu) && waitlevel << ch;
    ensures rd*(b.f);
  {
    receive b := ch
  }
  
  method t5(ch: C1)
    requires ch != null && acc(f,1);
    ensures true;
  {
    send ch(this)
    send ch(this)
    send ch(this)
  }
  
}

channel C1(x: C) where rd(x.f);
channel C2(x: C) where rd*(x.f);