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
|
import org.checkerframework.checker.initialization.qual.Initialized;
import org.checkerframework.checker.initialization.qual.NotOnlyInitialized;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;
public class SimpleFbc {
SimpleFbc f;
@NotOnlyInitialized SimpleFbc g;
@Pure
int pure() {
return 1;
}
// :: error: (initialization.fields.uninitialized)
public SimpleFbc(String arg) {}
void test() {
@NonNull String s = "234";
// :: error: (assignment.type.incompatible)
s = null;
System.out.println(s);
}
void test2(@UnknownInitialization @NonNull SimpleFbc t) {
// :: error: (assignment.type.incompatible)
@NonNull SimpleFbc a = t.f;
}
// check committed-only semantics for fields
void test3(@UnknownInitialization @NonNull SimpleFbc t) {
@Initialized @Nullable SimpleFbc a = t.f;
// :: error: (assignment.type.incompatible)
@Initialized @Nullable SimpleFbc b = t.g;
}
void simplestTestEver() {
@NonNull String a = "abc";
// :: error: (assignment.type.incompatible)
a = null;
// :: error: (assignment.type.incompatible)
@NonNull String b = null;
}
void anotherMethod() {
@Nullable String s = null;
@Initialized @Nullable String t = s;
}
}
|
