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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.*;
class PureTest {
@org.checkerframework.dataflow.qual.Pure
@Nullable Object puremethod(@Nullable Object a) {
return a;
}
public void test() {
// :: error: (assignment.type.incompatible)
@NonNull Object l0 = puremethod(null);
if (puremethod(null) == null) {
// :: error: (assignment.type.incompatible)
@NonNull Object l1 = puremethod(null);
}
if (puremethod("m") != null) {
@NonNull Object l1 = puremethod("m");
}
if (puremethod("m") != null) {
// :: error: (assignment.type.incompatible)
@NonNull Object l1 = puremethod(null);
}
if (puremethod("m") != null) {
// :: error: (assignment.type.incompatible)
@NonNull Object l1 = puremethod("n");
}
Object x = new Object();
if (puremethod(x) == null) {
return;
}
@NonNull Object l2 = puremethod(x);
x = new Object();
// :: error: (assignment.type.incompatible)
@NonNull Object l3 = puremethod(x);
// :: error: (assignment.type.incompatible)
@NonNull Object l4 = puremethod("n");
}
public @org.checkerframework.dataflow.qual.Pure @Nullable Object getSuperclass() {
return null;
}
static void shortCircuitAnd(PureTest pt) {
if ((pt.getSuperclass() != null) && pt.getSuperclass().equals(Enum.class)) {
// empty body
}
}
static void shortCircuitOr(PureTest pt) {
if ((pt.getSuperclass() == null) || pt.getSuperclass().equals(Enum.class)) {
// empty body
}
}
static void testInstanceofNegative(PureTest pt) {
if (pt.getSuperclass() instanceof Object) {
return;
}
// :: error: (dereference.of.nullable)
pt.getSuperclass().toString();
}
static void testInstanceofPositive(PureTest pt) {
if (!(pt.getSuperclass() instanceof Object)) {
return;
}
pt.getSuperclass().toString();
}
static void testInstanceofPositive2(PureTest pt) {
if (!(pt.getSuperclass() instanceof Object)) {
} else {
pt.getSuperclass().toString();
}
}
static void testInstanceofNegative2(PureTest pt) {
if (pt.getSuperclass() instanceof Object) {
} else {
return;
}
pt.getSuperclass().toString();
}
static void testInstanceofString(PureTest pt) {
if (!(pt.getSuperclass() instanceof String)) {
return;
}
pt.getSuperclass().toString();
}
static void testContinue(PureTest pt) {
for (; ; ) {
if (pt.getSuperclass() == null) {
System.out.println("m");
continue;
}
pt.getSuperclass().toString();
}
}
void setSuperclass(@Nullable Object no) {
// set the field returned by getSuperclass.
}
static void testInstanceofPositive3(PureTest pt) {
if (!(pt.getSuperclass() instanceof Object)) {
return;
} else {
pt.setSuperclass(null);
}
// :: error: (dereference.of.nullable)
pt.getSuperclass().toString();
}
@Override
@SideEffectFree
public String toString() {
return "foo";
}
}
|
