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
|
import org.checkerframework.checker.index.qual.*;
public class ArrayAssignmentSameLen {
private final int[] i_array;
private final @IndexFor("i_array") int i_index;
ArrayAssignmentSameLen(int[] array, @IndexFor("#1") int index) {
i_array = array;
i_index = index;
}
void test1(int[] a, int[] b, @LTEqLengthOf("#1") int index) {
int[] array = a;
@LTLengthOf(
value = {"array", "b"},
offset = {"0", "-3"})
// :: error: (assignment.type.incompatible)
int i = index;
}
void test2(int[] a, int[] b, @LTLengthOf("#1") int i) {
int[] c = a;
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = {"c", "b"}) int x = i;
@LTLengthOf("c") int y = i;
}
void test3(int[] a, @LTLengthOf("#1") int i, @NonNegative int x) {
int[] c1 = a;
// See useTest3 for an example of why this assignment should fail.
@LTLengthOf(
value = {"c1", "c1"},
offset = {"0", "x"})
// :: error: (assignment.type.incompatible)
int z = i;
}
void test4(
int[] a,
@LTLengthOf(
value = {"#1", "#1"},
offset = {"0", "#3"})
int i,
@NonNegative int x) {
int[] c1 = a;
@LTLengthOf(
value = {"c1", "c1"},
offset = {"0", "x"})
int z = i;
}
void useTest3() {
int[] a = {1, 3};
test3(a, 0, 10);
}
}
|
