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
|
import org.checkerframework.checker.nullness.qual.*;
// Test cases originally written by Dan Marino, UCLA, 10/8/2007.
@org.checkerframework.framework.qual.DefaultQualifier(Nullable.class)
public class Marino {
@NonNull String m_str;
static String ms_str;
String m_nullableStr;
public Marino(@NonNull String m_str, String m_nullableStr) {
this.m_str = m_str;
this.m_nullableStr = m_nullableStr;
}
void testWhile() throws Exception {
String s = "foo";
while (true) {
@NonNull String a = s;
System.out.println("a has length: " + a.length());
break;
}
int i = 1;
while (true) {
@NonNull String a = s; // s cannot be null here
s = null;
// :: error: (dereference.of.nullable)
System.out.println("hi" + s.length());
if (i > 2) break;
// :: error: (assignment.type.incompatible)
a = null;
}
// Checker doesn't catch that m_str not initialized.
// This is Caveat 2 in the manual, but note that it
// is not limited to contructors.
System.out.println("Member string has length: " + m_str.length());
// Dereference of any static field is allowed.
// I suppose this is a design decision
// for practicality in interacting with libraries...?
// :: error: (dereference.of.nullable)
System.out.println("Member string has length: " + ms_str.length());
System.out.println(
"Everyone should get this error: "
+
// :: error: (dereference.of.nullable)
m_nullableStr.length());
s = null;
@NonNull String b = "hi";
try {
System.out.println("b has length: " + b.length());
methodThatThrowsEx();
s = "bye";
} finally {
// Checker doesn't catch that s will be null here.
// :: error: (assignment.type.incompatible)
b = s;
System.out.println("b has length: " + b.length());
}
}
void methodThatThrowsEx() throws Exception {
throw new Exception();
}
}
|
