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
|
import org.checkerframework.common.aliasing.qual.*;
class ReceiverParameterTest {
public @Unique ReceiverParameterTest() {
nonLeaked();
// :: error: (unique.leaked)
mayLeak();
}
public @Unique ReceiverParameterTest(int i) {
leakedToResult();
// :: error: (unique.leaked)
ReceiverParameterTest b = leakedToResult();
}
public @Unique ReceiverParameterTest(String s) {}
void receiverTest() {
ReceiverParameterTest rec = new ReceiverParameterTest("s"); // @Unique
isUnique(rec);
rec.leakedToResult();
isUnique(rec);
ReceiverParameterTest other = rec.leakedToResult();
// :: error: (argument.type.incompatible)
isUnique(rec);
// :: error: (argument.type.incompatible)
isUnique(other);
}
void stubFileReceiverTest() {
// StringBuffer append(String s) @LeakedToResult;
StringBuffer sb = new StringBuffer();
isUnique(sb);
sb.append("something");
isUnique(sb);
StringBuffer sb2 = sb.append("something");
// :: error: (argument.type.incompatible)
isUnique(sb);
// :: error: (argument.type.incompatible)
isUnique(sb2);
}
ReceiverParameterTest leakedToResult(@LeakedToResult ReceiverParameterTest this) {
return this;
}
void nonLeaked(@NonLeaked ReceiverParameterTest this) {}
void mayLeak() {}
// @NonLeaked so it doesn't refine the type of the argument.
void isUnique(@NonLeaked @Unique ReceiverParameterTest s) {}
// @NonLeaked so it doesn't refine the type of the argument.
void isUnique(@NonLeaked @Unique String s) {}
// @NonLeaked so it doesn't refine the type of the argument.
void isUnique(@NonLeaked @Unique StringBuffer s) {}
}
|
