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
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
public class AssertIfFalseTest {
@org.checkerframework.dataflow.qual.Pure
@Nullable Object get() {
return "m";
}
@EnsuresNonNullIf(result = false, expression = "get()")
boolean isGettable() {
// don't bother with the implementation
// :: error: (contracts.conditional.postcondition.not.satisfied)
return false;
}
void simple() {
// :: error: (dereference.of.nullable)
get().toString();
}
void checkWrongly() {
if (isGettable()) {
// :: error: (dereference.of.nullable)
get().toString();
}
}
void checkCorrectly() {
if (!isGettable()) {
get().toString();
}
}
/** Returns whether or not constant_value is a legal constant. */
@EnsuresNonNullIf(result = false, expression = "#1")
static boolean legalConstant(final @Nullable Object constant_value) {
if ((constant_value == null)
|| ((constant_value instanceof Long) || (constant_value instanceof Double)))
return true;
return false;
}
void useLegalConstant1(@Nullable Object static_constant_value) {
if (!legalConstant(static_constant_value)) {
throw new AssertionError(
"unexpected constant class " + static_constant_value.getClass());
}
}
void useLegalConstant2(@Nullable Object static_constant_value) {
assert legalConstant(static_constant_value)
: "unexpected constant class " + static_constant_value.getClass();
}
}
|
