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
|
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
@org.checkerframework.framework.qual.DefaultQualifier(Nullable.class)
class RawMethodInvocation {
@NonNull String a;
@NonNull String b;
RawMethodInvocation(boolean constructor_inits_a) {
a = "";
init_b();
}
@EnsuresNonNull("b")
void init_b(@UnknownInitialization RawMethodInvocation this) {
b = "";
}
// :: error: (initialization.fields.uninitialized)
RawMethodInvocation(Byte constructor_inits_b) {
init_b();
}
// :: error: (initialization.fields.uninitialized)
RawMethodInvocation(byte constructor_inits_b) {
b = "";
init_b();
}
RawMethodInvocation(int constructor_inits_none) {
init_ab();
}
@EnsuresNonNull({"a", "b"})
void init_ab(@UnknownInitialization RawMethodInvocation this) {
a = "";
b = "";
}
RawMethodInvocation(long constructor_escapes_raw) {
a = "";
// :: error: (method.invocation.invalid)
nonRawMethod();
b = "";
}
void nonRawMethod() {}
}
|
