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
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
/*
* Miscellaneous tests based on problems found when checking Daikon.
*/
public class DaikonTests {
// Based on a problem found in PPtSlice.
class Bug1 {
@Nullable Object field;
public void cond1() {
if (this.hashCode() > 6 && Bug1Other.field != null) {
// spurious dereference error
Bug1Other.field.toString();
}
}
public void cond1(Bug1 p) {
if (this.hashCode() > 6 && p.field != null) {
// works
p.field.toString();
}
}
public void cond2() {
if (Bug1Other.field != null && this.hashCode() > 6) {
// works
Bug1Other.field.toString();
}
}
}
// Based on problem found in PptCombined.
// Not yet able to reproduce the problem :-(
class Bug2Data {
Bug2Data(Bug2Super o) {}
}
class Bug2Super {
public @MonotonicNonNull Bug2Data field;
}
class Bug2 extends Bug2Super {
private void m() {
field = new Bug2Data(this);
field.hashCode();
}
}
// Based on problem found in FloatEqual.
class Bug3 {
@EnsuresNonNullIf(expression = "derived", result = true)
public boolean isDerived() {
return (derived != null);
}
@Nullable Object derived;
void good1(Bug3 v1) {
if (!v1.isDerived() || !(5 > 9)) {
return;
}
v1.derived.hashCode();
}
// TODO: this is currently not supported
// void good2(Bug3 v1) {
// if (!(v1.isDerived() && (5 > 9)))
// return;
// v1.derived.hashCode();
// }
void good3(Bug3 v1) {
if (!v1.isDerived() || !(v1 instanceof Bug3)) {
return;
}
Object o = (Object) v1.derived;
o.hashCode();
}
}
// Based on problem found in PrintInvariants.
// Not yet able to reproduce the problem :-(
class Bug4 {
@MonotonicNonNull Object field;
void m(Bug4 p) {
if (false && p.field != null) {
p.field.hashCode();
}
}
}
// Based on problem found in chicory.Runtime:
class Bug5 {
@Nullable Object clazz;
@EnsuresNonNull("clazz")
void init() {
clazz = new Object();
}
void test(Bug5 b) {
if (b.clazz == null) {
b.init();
}
// The problem is:
// In the "then" branch, we have in "nnExpr" that "clazz" is non-null.
// In the "else" branch, we have in "annos" that the variable is non-null.
// However, as these are facts in two different representations, the merge keeps
// neither!
//
// no error message expected
b.clazz.hashCode();
}
}
// From LimitedSizeSet. The following initialization of the values array
// has caused a NullPointerException.
class Bug6<T> {
protected @Nullable T @Nullable [] values;
public Bug6() {
// :: warning: [unchecked] unchecked cast
@Nullable T[] new_values_array = (@Nullable T[]) new @Nullable Object[4];
values = new_values_array;
}
}
}
class Bug1Other {
static @Nullable Object field;
}
|
