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
|
import java.util.HashMap;
import java.util.List;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
public class AssertAfter2 {
public class Graph<T> {
HashMap<T, List<@KeyFor("childMap") T>> childMap;
public Graph(HashMap<T, List<@KeyFor("childMap") T>> childMap) {
this.childMap = childMap;
}
@SuppressWarnings("contracts.postcondition.not.satisfied")
@EnsuresNonNull("childMap.get(#1)")
public void addNode(final T n) {
// body omitted, not relevant to test case
}
public void addEdge(T parent, T child) {
addNode(parent);
@NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
}
public void addEdgeBad1(T parent, T child) {
// :: error: (assignment.type.incompatible)
@NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
}
public void addEdgeBad2(T parent, T child) {
addNode(parent);
// :: error: (assignment.type.incompatible)
@NonNull List<@KeyFor("childMap") T> l = childMap.get(child);
}
public void addEdgeBad3(T parent, T child) {
addNode(parent);
parent = child;
// :: error: (assignment.type.incompatible)
@NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
}
public void addEdgeOK(T parent, T child) {
List<@KeyFor("childMap") T> l = childMap.get(parent);
}
}
class MultiParam {
MultiParam(MultiParam thing, Object f1, Object f2, Object f3) {
this.thing = thing;
this.f1 = f1;
this.f2 = f2;
this.f3 = f3;
}
MultiParam thing;
@SuppressWarnings("contracts.postcondition.not.satisfied")
@EnsuresNonNull("get(#1, #2, #3)")
void add(final Object o1, final Object o2, final Object o3) {
// body omitted, not relevant to test case
}
@org.checkerframework.dataflow.qual.Pure
@Nullable Object get(Object o1, Object o2, Object o3) {
return null;
}
Object f1, f2, f3;
void addGood1() {
thing.add(f1, f2, f3);
@NonNull Object nn = thing.get(f1, f2, f3);
}
void addBad1() {
// :: error: (assignment.type.incompatible)
@NonNull Object nn = get(f1, f2, f3);
}
void addBad2() {
thing.add(f1, f2, f3);
f1 = new Object();
// :: error: (assignment.type.incompatible)
@NonNull Object nn = thing.get(f1, f2, f3);
}
void addBad3() {
thing.add(f1, f2, f3);
f2 = new Object();
// :: error: (assignment.type.incompatible)
@NonNull Object nn = thing.get(f1, f2, f3);
}
void addBad4() {
thing.add(f1, f2, f3);
f3 = new Object();
// :: error: (assignment.type.incompatible)
@NonNull Object nn = thing.get(f1, f2, f3);
}
}
}
|
