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.index.qual.*;
import org.checkerframework.dataflow.qual.Pure;
class SameLenManyArrays {
void transfer1(int @SameLen("#2") [] a, int[] b) {
int[] c = new int[a.length];
for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
b[i] = 1;
int @SameLen({"a", "b", "c"}) [] d = c;
}
}
void transfer2(int @SameLen("#2") [] a, int[] b) {
for (int i = 0; i < b.length; i++) { // i's type is @LTL("b")
a[i] = 1;
}
}
void transfer3(int @SameLen("#2") [] a, int[] b, int[] c) {
if (a.length == c.length) {
for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
b[i] = 1;
int @SameLen({"a", "b", "c"}) [] d = c;
}
}
}
void transfer4(int[] a, int[] b, int[] c) {
if (b.length == c.length) {
if (a.length == b.length) {
for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
a[i] = 1;
int @SameLen({"a", "b", "c"}) [] d = c;
}
}
}
}
void transfer5(int[] a, int[] b, int[] c, int[] d) {
if (a.length == b.length && b.length == c.length) {
int[] x = a;
int[] y = x;
int index = x.length - 1;
if (index > 0) {
f(a[index]);
f(b[index]);
f(c[index]);
f(x[index]);
f(y[index]);
}
}
}
@Pure
void f(Object o) {}
}
|