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
|
import org.checkerframework.checker.nullness.qual.*;
public class LazyInitialization {
@Nullable Object nullable;
@NonNull Object nonnull;
@MonotonicNonNull Object lazy;
@MonotonicNonNull Object lazy2 = null;
final @Nullable Object lazy3;
public LazyInitialization(@Nullable Object arg) {
lazy3 = arg;
nonnull = new Object();
}
void randomMethod() {}
void testAssignment() {
lazy = "m";
// :: error: (assignment.type.incompatible)
lazy = null; // null
}
void testLazyBeingNull() {
// :: error: (dereference.of.nullable)
nullable.toString(); // error
nonnull.toString();
// :: error: (dereference.of.nullable)
lazy.toString(); // error
// :: error: (dereference.of.nullable)
lazy3.toString(); // error
}
void testAfterInvocation() {
nullable = "m";
nonnull = "m";
lazy = "m";
if (lazy3 == null) {
return;
}
randomMethod();
// :: error: (dereference.of.nullable)
nullable.toString(); // error
nonnull.toString();
lazy.toString();
lazy3.toString();
}
private double @MonotonicNonNull [] intersect;
public void check_modified(double[] a, int count) {
if (intersect != null) {
double @NonNull [] nnda = intersect;
}
}
class PptRelation1 {
public void init_hierarchy_new(PptTopLevel ppt, Object eq) {
ppt.equality_view = eq;
ppt.equality_view.toString();
}
}
class PptTopLevel {
public @MonotonicNonNull Object equality_view;
}
class PptRelation1b {
// This is the same code as in PptRelation1, but comes after the class
// declaration of PptTopLevel. This works as expected.
public void init_hierarchy_new(PptTopLevel ppt, Object eq) {
ppt.equality_view = eq;
ppt.equality_view.toString();
}
}
class PptRelation2 {
public @MonotonicNonNull Object equality_view2;
public void init_hierarchy_new(PptRelation2 pr1, PptRelation2 pr2, Object eq) {
// :: error: (dereference.of.nullable)
pr1.equality_view2.toString();
pr1.equality_view2 = eq;
pr1.equality_view2.toString();
// :: error: (dereference.of.nullable)
pr2.equality_view2.toString();
// :: error: (dereference.of.nullable)
this.equality_view2.toString();
pr2.equality_view2 = eq;
pr2.equality_view2.toString();
this.equality_view2 = eq;
this.equality_view2.toString();
}
}
}
|
