Chalice/tests/permission-model/peculiar.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
46
47
48
49
50
51
52
53
54
55

class Cell {
  var x: int;
  
  invariant rd(x);
  
  method t1()
    requires acc(x);
    ensures rd(x) && rd(x);
  {
  }
  
  method t2()
    requires acc(x,1);
    ensures rd(x);
  {
    call void();
  }
  
  method t3()
    requires rd(x);
  {
    call t3helper();
  }
  
  method t3helper()
    requires rd(x) && rd(x);
    ensures rd(x) && rd(x);
  {}
  
  method t4()
    requires rd(x);
  {
    call dispose();
    call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
    assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
  }
  
  method t5(n: int)
    requires acc(x);
  {
    var i: int := 0;
    call req99();
    while (i < n)
      invariant rd*(x);
    {
      call dispose();
      i := i+1
    }
  }
    
  method dispose() requires rd(x); {}
  method void() requires rd(x); ensures rd(x); {}
  method req99() requires acc(x,99); {}

}