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
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
public class AssertAfterChecked {
class InitField {
@Nullable Object f;
@EnsuresNonNull("f")
void init() {
f = new Object();
}
@EnsuresNonNull("f")
// :: error: (contracts.postcondition.not.satisfied)
void initBad() {}
void testInit() {
init();
f.toString();
}
}
static class InitStaticField {
static @Nullable Object f;
@EnsuresNonNull("f")
void init() {
f = new Object();
}
@EnsuresNonNull("f")
void init2() {
InitStaticField.f = new Object();
}
@EnsuresNonNull("f")
// :: error: (contracts.postcondition.not.satisfied)
void initBad() {}
void testInit() {
init();
f.toString();
}
@EnsuresNonNull("InitStaticField.f")
void initE() {
f = new Object();
}
@EnsuresNonNull("InitStaticField.f")
void initE2() {
InitStaticField.f = new Object();
}
@EnsuresNonNull("InitStaticField.f")
// :: error: (contracts.postcondition.not.satisfied)
void initBadE() {}
void testInitE() {
initE();
// TODO: we need to also support the unqualified static field access?
// f.toString();
}
void testInitE2() {
initE();
InitStaticField.f.toString();
}
}
class TestParams {
@EnsuresNonNull("get(#1)")
// :: error: (contracts.postcondition.not.satisfied)
void init(final TestParams p) {}
@org.checkerframework.dataflow.qual.Pure
@Nullable Object get(Object o) {
return null;
}
void testInit1() {
init(this);
get(this).toString();
}
void testInit1b() {
init(this);
this.get(this).toString();
}
void testInit2(TestParams p) {
init(p);
get(p).toString();
}
void testInit3(TestParams p) {
p.init(this);
p.get(this).toString();
}
void testInit4(TestParams p) {
p.init(this);
// :: error: (dereference.of.nullable)
this.get(this).toString();
}
}
class WithReturn {
@Nullable Object f;
@EnsuresNonNull("f")
int init1() {
f = new Object();
return 0;
}
@EnsuresNonNull("f")
int init2() {
if (5 == 5) {
f = new Object();
return 0;
} else {
f = new Object();
return 1;
}
}
@EnsuresNonNull("f")
// :: error: (contracts.postcondition.not.satisfied)
int initBad1() {
return 0;
}
@EnsuresNonNull("f")
// :: error: (contracts.postcondition.not.satisfied)
int initBad2() {
if (5 == 5) {
return 0;
} else {
f = new Object();
return 1;
}
}
void testInit() {
init1();
f.toString();
}
}
}
|