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
|
import net.jcip.annotations.GuardedBy;
import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.checker.lock.qual.Holding;
import org.checkerframework.checker.lock.qual.LockingFree;
// Smoke test for supporting JCIP and Javax annotations.
// Note that JCIP and Javax @GuardedBy can only be written on fields and methods.
public class JCIPAnnotations {
class MyClass {
Object field;
@LockingFree
void methodWithUnguardedReceiver() {}
@LockingFree
void methodWithGuardedReceiver(
@org.checkerframework.checker.lock.qual.GuardedBy("lock") MyClass this) {}
@LockingFree
void methodWithGuardSatisfiedReceiver(@GuardSatisfied MyClass this) {}
}
final Object lock = new Object();
@GuardedBy("lock") MyClass jcipGuardedField;
@javax.annotation.concurrent.GuardedBy("lock") MyClass javaxGuardedField;
// Tests that Javax and JCIP @GuardedBy(...) typecheck against the Lock Checker @GuardedBy on a
// receiver.
void testReceivers() {
// :: error: (method.invocation.invalid)
jcipGuardedField.methodWithUnguardedReceiver();
jcipGuardedField.methodWithGuardedReceiver();
// :: error: (lock.not.held)
jcipGuardedField.methodWithGuardSatisfiedReceiver();
// :: error: (method.invocation.invalid)
javaxGuardedField.methodWithUnguardedReceiver();
javaxGuardedField.methodWithGuardedReceiver();
// :: error: (lock.not.held)
javaxGuardedField.methodWithGuardSatisfiedReceiver();
}
void testDereferences() {
// :: error: (lock.not.held)
this.jcipGuardedField.field.toString();
// :: error: (lock.not.held)
this.javaxGuardedField.field.toString();
synchronized (lock) {
this.jcipGuardedField.field.toString();
this.javaxGuardedField.field.toString();
}
}
@GuardedBy("lock")
void testGuardedByAsHolding() {
this.jcipGuardedField.field.toString();
this.javaxGuardedField.field.toString();
jcipGuardedField.field.toString();
javaxGuardedField.field.toString();
}
@GuardedBy("lock") Object testGuardedByAsHolding2(
@org.checkerframework.checker.lock.qual.GuardedBy({}) Object param) {
testGuardedByAsHolding();
// Test that the JCIP GuardedBy applies to the method but not the return type.
return param;
}
void testGuardedByAsHolding3() {
synchronized (lock) {
testGuardedByAsHolding();
}
// :: error: (contracts.precondition.not.satisfied)
testGuardedByAsHolding();
}
@Holding("lock")
@GuardedBy("lock")
// :: error: (multiple.lock.precondition.annotations)
void testMultipleMethodAnnotations1() {}
@Holding("lock")
@javax.annotation.concurrent.GuardedBy("lock")
// :: error: (multiple.lock.precondition.annotations)
void testMultipleMethodAnnotations2() {}
@GuardedBy("lock") @javax.annotation.concurrent.GuardedBy("lock")
// :: error: (multiple.lock.precondition.annotations)
void testMultipleMethodAnnotations3() {}
@Holding("lock")
@GuardedBy("lock") @javax.annotation.concurrent.GuardedBy("lock")
// :: error: (multiple.lock.precondition.annotations)
void testMultipleMethodAnnotations4() {}
@GuardedBy("lock") @org.checkerframework.checker.lock.qual.GuardedBy("lock")
// :: error: (multiple.guardedby.annotations)
Object fieldWithMultipleGuardedByAnnotations1;
@javax.annotation.concurrent.GuardedBy("lock") @org.checkerframework.checker.lock.qual.GuardedBy("lock")
// :: error: (multiple.guardedby.annotations)
Object fieldWithMultipleGuardedByAnnotations2;
@GuardedBy("lock") @javax.annotation.concurrent.GuardedBy("lock")
// :: error: (multiple.guardedby.annotations)
Object fieldWithMultipleGuardedByAnnotations3;
@GuardedBy("lock") @javax.annotation.concurrent.GuardedBy("lock") @org.checkerframework.checker.lock.qual.GuardedBy("lock")
// :: error: (multiple.guardedby.annotations)
Object fieldWithMultipleGuardedByAnnotations4;
}
|
