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
|
import org.checkerframework.checker.nullness.qual.AssertNonNullIfNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.Pure;
// Re-enable when @AssertNonNullIfNonNull checking is enhanced
// @skip-test
public class AssertNonNullIfNonNullTest {
private @Nullable String value;
@Pure
@AssertNonNullIfNonNull("value")
public @Nullable String getValue() {
return value;
}
public void setValue(String value) {
this.value = value;
}
@EnsuresNonNullIf(expression = "value", result = true)
public boolean isValueNonNull1() {
return value != null;
}
@EnsuresNonNullIf(expression = "getValue()", result = true)
public boolean isValueNonNull2() {
// The @AssertNonNullIfNonNull annotation implies that if getValue() is
// non-null, then is non-null, then value is non-null, but not the
// converse, so an error should be issued here.
// :: error: (contracts.conditional.postcondition.not.satisfied)
return value != null;
}
// The @AssertNonNullIfNonNull annotation should enable suppressing this error.
@EnsuresNonNullIf(expression = "value", result = true)
public boolean isValueNonNull3() {
return getValue() != null;
}
@EnsuresNonNullIf(expression = "getValue()", result = true)
public boolean isValueNonNull4() {
return getValue() != null;
}
}
|
