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.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
public class AssertWithStatic {
static @Nullable String f;
@EnsuresNonNullIf(result = true, expression = "AssertWithStatic.f")
public boolean hasSysOut1() {
return AssertWithStatic.f != null;
}
@EnsuresNonNullIf(result = true, expression = "f")
public boolean hasSysOut2() {
return AssertWithStatic.f != null;
}
@EnsuresNonNullIf(result = true, expression = "AssertWithStatic.f")
public boolean hasSysOut3() {
return f != null;
}
@EnsuresNonNullIf(result = true, expression = "f")
public boolean hasSysOut4() {
return f != null;
}
@EnsuresNonNullIf(result = false, expression = "AssertWithStatic.f")
public boolean noSysOut1() {
return AssertWithStatic.f == null;
}
@EnsuresNonNullIf(result = false, expression = "f")
public boolean noSysOut2() {
return AssertWithStatic.f == null;
}
@EnsuresNonNullIf(result = false, expression = "AssertWithStatic.f")
public boolean noSysOut3() {
return f == null;
}
@EnsuresNonNullIf(result = false, expression = "f")
public boolean noSysOut4() {
return f == null;
}
@EnsuresNonNull("AssertWithStatic.f")
// :: error: (contracts.postcondition.not.satisfied)
public void sysOutAfter1() {}
@EnsuresNonNull("f")
// :: error: (contracts.postcondition.not.satisfied)
public void sysOutAfter2() {}
}
|
