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)
}
}
|
