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
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.Pure;
class RequiresNonNullTest {
@Nullable Object field1;
@Nullable Object field2;
@RequiresNonNull("field1")
void method1() {
field1.toString(); // OK, field1 is known to be non-null
this.field1.toString(); // OK, field1 is known to be non-null
// :: error: (dereference.of.nullable)
field2.toString(); // error, might throw NullPointerException
}
@RequiresNonNull("field1")
void method1also() {
// ok, precondition satisfied by NNOE
method1();
}
void method2() {
field1 = new Object();
method1(); // OK, satisfies method precondition
field1 = null;
// :: error: (contracts.precondition.not.satisfied)
method1(); // error, does not satisfy method precondition
}
protected @Nullable Object field;
@RequiresNonNull("field")
public void requiresNonNullField() {}
public void clientFail(RequiresNonNullTest arg1) {
// :: error: (contracts.precondition.not.satisfied)
arg1.requiresNonNullField();
}
public void clientOK(RequiresNonNullTest arg2) {
arg2.field = new Object();
// note that the following line works
@NonNull Object o = arg2.field;
arg2.requiresNonNullField(); // OK, field is known to be non-null
}
// TODO: forbid the field in @NNOE to be less visible than the method
protected static @Nullable Object staticfield;
@Pure
@RequiresNonNull("staticfield")
// :: warning: (purity.deterministic.void.method)
public void reqStaticName() {
reqStaticQualName();
}
@Pure
@RequiresNonNull("RequiresNonNullTest.staticfield")
// :: warning: (purity.deterministic.void.method)
public void reqStaticQualName() {
reqStaticName();
}
public void statClientOK(RequiresNonNullTest arg1) {
staticfield = new Object();
arg1.reqStaticName();
staticfield = new Object();
arg1.reqStaticQualName();
RequiresNonNullTest.staticfield = new Object();
arg1.reqStaticName();
RequiresNonNullTest.staticfield = new Object();
arg1.reqStaticQualName();
}
public void statClientFail(RequiresNonNullTest arg1) {
// :: error: (contracts.precondition.not.satisfied)
arg1.reqStaticName();
// :: error: (contracts.precondition.not.satisfied)
arg1.reqStaticQualName();
}
class NNOESubTest extends RequiresNonNullTest {
public void subClientOK(NNOESubTest arg3) {
arg3.field = new Object();
arg3.requiresNonNullField();
}
public void subClientFail(NNOESubTest arg4) {
// :: error: (contracts.precondition.not.satisfied)
arg4.requiresNonNullField();
}
public void subStat(NNOESubTest arg5) {
RequiresNonNullTest.staticfield = new Object();
arg5.reqStaticQualName();
staticfield = new Object();
arg5.reqStaticQualName();
NNOESubTest.staticfield = new Object();
arg5.reqStaticQualName();
}
}
private @Nullable Object notHidden;
class NNOEHidingTest extends RequiresNonNullTest {
protected @Nullable String field;
public void hidingClient1(NNOEHidingTest arg5) {
arg5.field = "ha!";
/* We should be testing that the Object "field" from the superclass
* is non-null. We currently only match on the field name and do not
* handle hiding correctly. Instead, we output an error, if we
* detect that hiding happened.
* TODO: correctly resolve hidden fields.
*/
arg5.requiresNonNullField();
}
public void hidingClient2(NNOEHidingTest arg6) {
// :: error: (contracts.precondition.not.satisfied)
arg6.requiresNonNullField();
}
protected @Nullable Object notHidden;
@RequiresNonNull("notHidden")
void notHiddenTest() {
// the field in the superclass is private -> don't complain about hiding
}
}
static @Nullable Object o = "m";
@RequiresNonNull("o")
void test() {
o = null;
}
@RequiresNonNull("thisShouldIssue1Error")
// Test case for Issue 1051
// https://github.com/typetools/checker-framework/issues/1051
// :: error: (flowexpr.parse.error)
void testIssue1051() {}
}
|