summaryrefslogtreecommitdiff
path: root/Chalice/examples/prog1.chalice
blob: 133de36d713fa09bbbe2d9f97c0f54569704bb43 (plain)
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
// 7 errors expected

class C {
  var x: int;
  invariant acc(x) && 0 <= x;

  method seq0() returns (r: int)
  {
    r := x;  // error: cannot access this.x here (90)
  }
  method seq1() returns (r: int)
    requires acc(x);
  {
    r := x;
  }
  method seq2() returns (r: int)
    requires rd(x);
  {
    r := x;
  }
  method seq3() returns (r: int)
    requires rd(x);
  {
    r := x;
    x := x + 1;  // error: cannot write to this.x here (184)
  }

  method main0()
  {
    var c := new C;
    c.x := 0;
    share c;
    var t := c.x;  // error: cannot access c.x now (254)
  }
  method main1()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x - 1;
    release c;  // error: monitor invariant might not hold (362)
  }
  method main2()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x + 1;
    release c;  // good!
  }
  method main3()
  {
    var c := new C;
    c.x := 2;
    share c;
    rd acquire c;
    var tmp := c.x + 1;  // fine
    c.x := tmp;  // error: cannot write to c.x here (582)
    rd release c;
  }
  method main4()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x + 1;
    unshare c;
    c.x := c.x + 1;
  }
  method main5()
  {
    var c := new C;
    unshare c;  // error: cannot unshare an object that isn't shared (754)
  }
  method main6()
  {
    var c := new C;
    c.x := 0;
    share c;  acquire c;
    unshare c;
    unshare c;  // error: cannot unshare an object that isn't shared (862)
  }
}