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
|
// Test case for https://github.com/kelloggm/checker-framework/issues/158
// It is easy to see that:
// * i is an index for intermediate
// * length <= i (or, at least length <= i+1)
// but I don't see how to verif that length is an index for intermediate.
// @skip-test
import org.checkerframework.checker.index.qual.IndexOrHigh;
public class VarLteVar {
/** Returns an array that is equivalent to the set difference of seq1 and seq2. */
public static boolean[] setDiff(boolean[] seq1, boolean[] seq2) {
boolean[] intermediate = new boolean[seq1.length];
int length = 0;
for (int i = 0; i < seq1.length; i++) {
if (!memberOf(seq1[i], seq2)) {
intermediate[length++] = seq1[i];
}
}
return subarray(intermediate, 0, length);
}
public static boolean memberOf(boolean elt, boolean[] arr) {
for (int i = 0; i < arr.length; i++) {
if (arr[i] == elt) {
return true;
}
}
return false;
}
@SuppressWarnings("index") // not relevant to this test case
public static boolean[] subarray(
boolean[] a, @IndexOrHigh("#1") int startindex, @IndexOrHigh("#1") int length) {
boolean[] result = new boolean[length];
System.arraycopy(a, startindex, result, 0, length);
return result;
}
}
|
