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
|
import java.util.concurrent.locks.*;
import org.checkerframework.checker.lock.qual.*;
import org.checkerframework.framework.qual.AnnotatedFor;
public class BasicLockTest {
class MyClass {
public Object field;
}
MyClass myUnannotatedMethod(MyClass param) {
return param;
}
void myUnannotatedMethod2() {}
@AnnotatedFor("lock")
MyClass myAnnotatedMethod(MyClass param) {
return param;
}
@AnnotatedFor("lock")
void myAnnotatedMethod2() {}
final @GuardedBy({}) ReentrantLock lockField = new ReentrantLock();
@GuardedBy("lockField") MyClass m;
@GuardedBy({}) MyClass o1 = new MyClass(), p1;
@AnnotatedFor("lock")
@MayReleaseLocks
void testFields() {
// Test in two ways that return values are @GuardedByUnknown.
// The first way is more durable as cannot.dereference is tied specifically to
// @GuardedByUnknown (and @GuardedByBottom, but it is unlikely to become the default for
// return values on unannotated methods).
// :: error: (lock.not.held)
myUnannotatedMethod(o1).field = new Object();
// The second way is less durable because the default for fields is currently @GuardedBy({})
// but could be changed to @GuardedByUnknown.
// :: error: (assignment.type.incompatible)
p1 = myUnannotatedMethod(o1);
// Now test that an unannotated method behaves as if it's annotated with @MayReleaseLocks
lockField.lock();
myAnnotatedMethod2();
m.field = new Object();
myUnannotatedMethod2();
// :: error: (lock.not.held)
m.field = new Object();
}
void unannotatedReleaseLock(ReentrantLock lock) {
lock.unlock();
}
@AnnotatedFor("lock")
@MayReleaseLocks
void testLocalVariables() {
MyClass o2 = new MyClass(), p2;
p2 = myUnannotatedMethod(o2);
MyClass o3 = new MyClass();
myAnnotatedMethod(o3);
// Now test that an unannotated method behaves as if it's annotated with @MayReleaseLocks
final @GuardedBy({}) ReentrantLock lock = new ReentrantLock();
@GuardedBy("lock") MyClass q = new MyClass();
lock.lock();
myAnnotatedMethod2();
q.field = new Object();
// Should behave as @MayReleaseLocks, and *should* reset @LockHeld assumption about local
// variable lock.
myUnannotatedMethod2();
// :: error: (lock.not.held)
q.field = new Object();
lock.lock();
// Should behave as @MayReleaseLocks, and *should* reset @LockHeld assumption about local
// variable lock.
unannotatedReleaseLock(lock);
// :: error: (lock.not.held)
q.field = new Object();
}
}
|
