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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
import org.checkerframework.checker.lock.qual.*;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.*;
class ItselfExpressionCases {
final Object somelock = new Object();
private final @GuardedBy({"<self>"}) MyClass m = new MyClass();
@Pure
private @GuardedBy({"<self>"}) MyClass getm() {
return m;
}
@Pure
private @GuardedBy({"<self>"}) MyClass getm2(@GuardedBy("<self>") ItselfExpressionCases this) {
// The following error is due to the precondition of the this.m field dereference not being
// satisfied.
// :: error: (lock.not.held)
return m;
}
@Pure
private Object getmfield() {
// :: error: (lock.not.held)
return getm().field;
}
public void arrayTest(final Object @GuardedBy("<self>") [] a1) {
// :: error: (lock.not.held)
Object a = a1[0];
synchronized (a1) {
a = a1[0];
}
}
Object @GuardedBy("<self>") [] a2;
@Pure
public Object @GuardedBy("<self>") [] geta2() {
return a2;
}
public void arrayTest() {
// :: error: (lock.not.held)
Object a = geta2()[0];
synchronized (geta2()) {
a = geta2()[0];
}
}
public void testCheckPreconditions(
final @GuardedBy("<self>") MyClass o,
@GuardSatisfied Object gs,
@GuardSatisfied MyClass gsMyClass) {
// :: error: (lock.not.held)
getm().field = new Object();
synchronized (getm()) {
getm().field = new Object();
}
// :: error: (lock.not.held)
m.field = new Object();
synchronized (m) {
m.field = new Object();
}
// :: error: (lock.not.held)
gs = m.field;
synchronized (m) {
gs = m.field;
}
// :: error: (lock.not.held)
gs = getm().field;
synchronized (getm()) {
gs = getm().field;
}
// :: error: (lock.not.held)
gsMyClass = getm();
synchronized (getm()) {
gsMyClass = getm();
}
// :: error: (lock.not.held) :: error: (contracts.precondition.not.satisfied)
o.foo();
synchronized (o) {
// :: error: (contracts.precondition.not.satisfied)
o.foo();
synchronized (somelock) {
o.foo();
}
}
// :: error: (lock.not.held)
o.foo2();
synchronized (o) {
o.foo2();
}
}
class MyClass {
Object field = new Object();
@Holding("somelock")
void foo(@GuardSatisfied MyClass this) {}
void foo2(@GuardSatisfied MyClass this) {}
void method(@GuardedBy("<self>") MyClass this) {
// :: error: (lock.not.held) :: error: (contracts.precondition.not.satisfied)
this.foo();
// :: error: (lock.not.held):: error: (contracts.precondition.not.satisfied)
foo();
// :: error: (lock.not.held)
synchronized (somelock) {
// :: error: (lock.not.held)
this.foo();
// :: error: (lock.not.held)
foo();
synchronized (this) {
this.foo();
foo();
}
}
// :: error: (lock.not.held)
this.foo2();
// :: error: (lock.not.held)
foo2();
synchronized (this) {
this.foo2();
foo2();
}
}
}
}
|
