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
|
import java.util.HashMap;
import java.util.Map;
import org.checkerframework.checker.nullness.qual.EnsuresKeyForIf;
import org.checkerframework.checker.nullness.qual.KeyFor;
public class Issue2619b {
public Map<String, String> map = new HashMap<>();
void m01(Aux aux1, Aux aux2) {
if (aux1.hasValue(Aux.MINIMUM_VALUE) && aux2.hasValue(Aux.MINIMUM_VALUE)) {
// hasValue is not sideeffect free, so the @KeyFor("aux1.map") is cleared rather than
// glb'ed.
// :: error: (assignment.type.incompatible)
@KeyFor({"aux1.map", "aux2.map"}) String s1 = Aux.MINIMUM_VALUE;
}
}
void m02(Aux aux1, Aux aux2) {
if (aux1.hasValue(Aux.MINIMUM_VALUE) && aux2.hasValue(Aux.MINIMUM_VALUE)) {
@KeyFor("aux2.map") String s1 = Aux.MINIMUM_VALUE;
}
}
void m03(Aux aux1, Aux aux2) {
if (aux1.hasValue(Aux.MINIMUM_VALUE) && map.containsKey(Aux.MINIMUM_VALUE)) {
// ok because map.containsKey is sideeffect free.
@KeyFor({"aux1.map", "map"}) String s1 = Aux.MINIMUM_VALUE;
@KeyFor("map") String s2 = Aux.MINIMUM_VALUE;
}
}
void m04(Aux aux1, Aux aux2) {
if (map.containsKey(Aux.MINIMUM_VALUE) && aux1.hasValue(Aux.MINIMUM_VALUE)) {
// :: error: (assignment.type.incompatible)
@KeyFor({"aux1.map", "map"}) String s1 = Aux.MINIMUM_VALUE;
@KeyFor("aux1.map") String s2 = Aux.MINIMUM_VALUE;
}
}
static class Aux {
public Map<String, String> map = new HashMap<>();
public static String MINIMUM_VALUE = "minvalue";
@EnsuresKeyForIf(result = true, expression = "#1", map = "map")
public boolean hasValue(String key) {
return map.containsKey(key);
}
public int getInt(@KeyFor("this.map") String key) {
return 22;
}
}
}
|
