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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
import java.util.List;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.framework.test.*;
import testlib.util.*;
class Basic2 {
// basic tests to make sure everything works
void t1(@Odd String p1, String p2) {
String l1 = p1;
// :: error: (assignment.type.incompatible)
@Odd String l2 = p2;
}
// basic local variable flow sensitivity
void t2(@Odd String p1, String p2, boolean b1) {
String l1 = p1;
if (b1) {
l1 = p2;
}
// :: error: (assignment.type.incompatible)
@Odd String l3 = l1;
l1 = p1;
while (b1) {
l1 = p2;
}
// :: error: (assignment.type.incompatible)
@Odd String l4 = l1;
}
void t2b(@Odd String p1, String p2, @Odd String p3, boolean b1) {
String l1 = p1;
if (b1) {
l1 = p3;
}
@Odd String l3 = l1;
while (b1) {
l1 = p3;
}
@Odd String l4 = l1;
}
// return statement
void t3(@Odd String p1, String p2, boolean b1) {
String l1 = p1;
if (b1) {
l1 = p2;
return;
}
@Odd String l3 = l1;
}
// simple throw statement
void t4(@Odd String p1, String p2, boolean b1) {
String l1 = p1;
if (b1) {
l1 = p2;
throw new RuntimeException();
}
@Odd String l3 = l1;
}
class C {
C c;
String f1, f2, f3;
@Odd String g1, g2, g3;
}
// fields
void t5(@Odd String p1, String p2, boolean b1, C c1, C c2) {
c1.f1 = p1;
@Odd String l1 = c1.f1;
c2.f2 = p2; // assignment to f2 does not change knowledge about f1
c1.f2 = p2;
@Odd String l2 = c1.f1;
c2.f1 = p2;
// :: error: (assignment.type.incompatible)
@Odd String l3 = c1.f1;
}
// fields
void t6(@Odd String p1, String p2, boolean b1, C c1, C c2) {
c1.f1 = p1;
c1.c.f1 = p1;
@Odd String l2 = c1.c.f1;
c1.f1 = p2;
// :: error: (assignment.type.incompatible)
@Odd String l3 = c1.f1;
c1.f1 = p1;
c1.c.f1 = p1;
@Odd String l4 = c1.c.f1;
c2.c = c2;
// :: error: (assignment.type.incompatible)
@Odd String l5 = c1.f1;
// :: error: (assignment.type.incompatible)
@Odd String l6 = c1.c.f1;
}
// fields
void t6b(@Odd String p1, String p2, boolean b1, C c1, C c2) {
if (b1) {
c1.f1 = p1;
}
// :: error: (assignment.type.incompatible)
@Odd String l1 = c1.f1;
if (b1) {
c1.f1 = p1;
} else {
c1.f1 = p1;
}
@Odd String l2 = c1.f1;
}
// method calls
void nonpure() {}
@Pure
int pure() {
return 1;
}
void t7(@Odd String p1, String p2, boolean b1, C c1, C c2) {
c1.f1 = p1;
nonpure();
// :: error: (assignment.type.incompatible)
@Odd String l1 = c1.f1;
c1.f1 = p1;
pure();
@Odd String l2 = c1.f1;
}
// array accesses
void t8(@Odd String a1[], String a2[], String p3) {
String l1 = a1[0];
// :: error: (assignment.type.incompatible)
@Odd String l2 = a2[0];
@Odd String l3 = l1;
a1[0] = l1;
a1[1] = l3;
// :: error: (assignment.type.incompatible)
a1[2] = p3;
a2[0] = l1;
a2[1] = l3;
a2[2] = p3;
}
// self type
void t9(@Odd Basic2 this) {
@Odd Basic2 l1 = this;
}
// generics
public <T extends String> void t10a(T p1, @Odd T p2) {
T l1 = p1;
p1 = l1;
T l2 = p2;
p2 = l2;
// :: error: (assignment.type.incompatible)
@Odd T l3 = p1;
@Odd T l4 = p2;
}
public <T extends @Odd String> void t10b(T p1, @Odd T p2) {
T l1 = p1;
p1 = l1;
T l2 = p2;
p2 = l2;
@Odd T l3 = p1;
@Odd T l4 = p2;
}
// for-each loop
void t11(@Odd String p1, String p2, List<String> list, List<@Odd String> oddList) {
// :: error: (enhancedfor.type.incompatible)
for (@Odd String i : list) {}
for (@Odd String i : oddList) {
@Odd String l1 = i;
}
for (@Odd String i : oddList) {
// :: error: (assignment.type.incompatible)
i = p2;
}
for (String i : oddList) {
// @Odd String l3 = i;
}
}
// cast without annotations
void t12(@Odd String p1, String p2, boolean b1) {
@Odd String l1 = (String) p1;
}
// final fields
class CF {
final String f1;
CF c;
void nonpure() {};
CF(@Odd String p1) {
f1 = p1;
nonpure();
@Odd String l1 = f1;
}
void CF_t1(@Odd String p1, CF o) {
if (f1 == p1) {
nonpure();
@Odd String l1 = f1;
}
}
}
// final fields with initializer
class A {
final @Odd String f1 = null;
final String f2 = f1;
void A_t1() {
@Odd String l1 = f2;
}
}
}
|
