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
|
import java.util.Collections;
import java.util.Set;
import org.checkerframework.checker.initialization.qual.*;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
class NNOEStaticFields {
static @Nullable String nullable = null;
static @Nullable String otherNullable = null;
@RequiresNonNull("nullable")
void testF() {
nullable.toString();
}
@RequiresNonNull("NNOEStaticFields.nullable")
void testF2() {
nullable.toString();
}
@RequiresNonNull("nullable")
void testF3() {
NNOEStaticFields.nullable.toString();
}
@RequiresNonNull("NNOEStaticFields.nullable")
void testF4() {
NNOEStaticFields.nullable.toString();
}
class Inner {
void m1(NNOEStaticFields out) {
NNOEStaticFields.nullable = "haha!";
out.testF4();
}
@RequiresNonNull("NNOEStaticFields.nullable")
void m2(NNOEStaticFields out) {
out.testF4();
}
}
@RequiresNonNull("NoClueWhatThisShouldBe")
// :: error: (flowexpr.parse.error)
void testF5() {
// :: error: (dereference.of.nullable)
NNOEStaticFields.nullable.toString();
}
void trueNegative() {
// :: error: (dereference.of.nullable)
nullable.toString();
// :: error: (dereference.of.nullable)
otherNullable.toString();
}
@RequiresNonNull("nullable")
void test1() {
nullable.toString();
// :: error: (dereference.of.nullable)
otherNullable.toString();
}
@RequiresNonNull("otherNullable")
void test2() {
// :: error: (dereference.of.nullable)
nullable.toString();
otherNullable.toString();
}
@RequiresNonNull({"nullable", "otherNullable"})
void test3() {
nullable.toString();
otherNullable.toString();
}
@RequiresNonNull("System.out")
void test4() {
@NonNull Object f = System.out;
}
///////////////////////////////////////////////////////////////////////////
/// Copied from Daikon's ChicoryPremain
///
static class ChicoryPremain1 {
// Non-null if doPurity == true
private static @MonotonicNonNull Set<String> pureMethods = null;
private static boolean doPurity = false;
@EnsuresNonNullIf(result = true, expression = "ChicoryPremain1.pureMethods")
// this postcondition cannot be proved with the Checker Framework, as the relation
// between doPurity and pureMethods is not explicit
public static boolean shouldDoPurity() {
// :: error: (contracts.conditional.postcondition.not.satisfied)
return doPurity;
}
@RequiresNonNull("ChicoryPremain1.pureMethods")
public static Set<String> getPureMethods() {
return Collections.unmodifiableSet(pureMethods);
}
}
static class ClassInfo1 {
public void initViaReflection() {
if (ChicoryPremain1.shouldDoPurity()) {
for (String pureMeth : ChicoryPremain1.getPureMethods()) {}
}
}
}
}
|
