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
|
import java.util.Arrays;
import org.checkerframework.checker.index.qual.*;
class SearchIndexTests {
public void test(short[] a, short instant) {
int i = Arrays.binarySearch(a, instant);
@SearchIndexFor("a") int z = i;
// :: error: (assignment.type.incompatible)
@SearchIndexFor("a") int y = 7;
@LTLengthOf("a") int x = i;
}
void test2(int[] a, @SearchIndexFor("#1") int xyz) {
if (0 > xyz) {
@NegativeIndexFor("a") int w = xyz;
@NonNegative int y = ~xyz;
@LTEqLengthOf("a") int z = ~xyz;
}
}
void test3(int[] a, @SearchIndexFor("#1") int xyz) {
if (-1 >= xyz) {
@NegativeIndexFor("a") int w = xyz;
@NonNegative int y = ~xyz;
@LTEqLengthOf("a") int z = ~xyz;
}
}
void test4(int[] a, @SearchIndexFor("#1") int xyz) {
if (xyz < 0) {
@NegativeIndexFor("a") int w = xyz;
@NonNegative int y = ~xyz;
@LTEqLengthOf("a") int z = ~xyz;
}
}
void test5(int[] a, @SearchIndexFor("#1") int xyz) {
if (xyz <= -1) {
@NegativeIndexFor("a") int w = xyz;
@NonNegative int y = ~xyz;
@LTEqLengthOf("a") int z = ~xyz;
}
}
void subtyping1(
@SearchIndexFor({"#3", "#4"}) int x, @NegativeIndexFor("#3") int y, int[] a, int[] b) {
// :: error: (assignment.type.incompatible)
@SearchIndexFor({"a", "b"}) int z = y;
@SearchIndexFor("a") int w = y;
@SearchIndexFor("b") int p = x;
// :: error: (assignment.type.incompatible)
@NegativeIndexFor({"a", "b"}) int q = x;
}
}
|
