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
|
import java.util.List;
import org.checkerframework.checker.nullness.qual.*;
@org.checkerframework.framework.qual.DefaultQualifier(Nullable.class)
class Explosion {
public static class ExplosiveException extends Exception {}
@NonNull Integer m_nni = 1;
final String m_astring;
Explosion() {
// m_nni = 1;\
m_astring = "hi";
try {
throw new RuntimeException();
} catch (Exception e) {
System.out.println(m_astring.length());
}
return;
}
static void main(String @NonNull [] args) {
@NonNull String s = "Dan";
String s2;
s2 = null;
// :: warning: (known.nonnull)
if (s2 != null || s != null) {
// :: error: (assignment.type.incompatible)
s = s2;
} else {
s = new String("Levitan");
}
s2 = args[0];
// :: error: (dereference.of.nullable)
System.out.println("Possibly cause null pointer with this: " + s2.length());
// :: warning: (known.nonnull)
if (s2 == null) {
// do nothing
} else {
System.out.println("Can't cause null pointer here: " + s2.length());
s = s2;
}
// :: warning: (known.nonnull)
if (s == null ? s2 != null : s2 != null) {
s = s2;
}
System.out.println("Hello " + s);
System.out.println("Hello " + s.length());
f();
}
private static int f() {
while (true) {
try {
throw new ExplosiveException();
} finally {
// break;
return 1;
// throw new RuntimeException();
}
}
}
public static int foo() {
final int v;
int x;
Integer z;
Integer y;
@NonNull Integer nnz = 3;
z = Integer.valueOf(5);
try {
x = 3;
x = 5;
// y = z;
nnz = z;
z = null;
// :: error: (assignment.type.incompatible)
nnz = z;
while (z == null) {
break;
}
// :: error: (assignment.type.incompatible)
nnz = z;
while (z == null) {
// do nothing
}
nnz = z;
// v = 1;
return 1;
// v = 2;
// throw new RuntimeException ();
} catch (NullPointerException e) {
e.printStackTrace();
// e = null;
// v = 1;
} catch (RuntimeException e) {
// nnz = z;
// v = 2;
} finally {
// v = 1 + x;
}
return 1;
// return v + x;
}
private void bar(List<@NonNull String> ss, String b, String c) {
@NonNull String a;
// :: error: (iterating.over.nullable)
for (@NonNull String s : ss) {
a = s;
}
if (b == null || b.length() == 0) {
System.out.println("hey");
}
if (b != null) {
// :: error: (dereference.of.nullable)
for (; b.length() > 0; b = null) {
System.out.println(b.length());
}
}
}
}
|
