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
|
// Test case for issue 98: https://github.com/kelloggm/checker-framework/issues/98
import org.checkerframework.checker.index.qual.*;
public class SubtractingNonNegatives {
public static void m4(int[] a, @IndexFor("#1") int i, @IndexFor("#1") int j) {
int k = i;
if (k >= j) {
@IndexFor("a") int y = k;
}
for (k = i; k >= j; k -= j) {
@IndexFor("a") int x = k;
}
}
@SuppressWarnings("lowerbound")
void test(int[] a, @Positive int y) {
@LTLengthOf("a") int x = a.length - 1;
@LTLengthOf(
value = {"a", "a"},
offset = {"0", "y"})
int z = x - y;
a[z + y] = 0;
}
@SuppressWarnings("lowerbound")
void test2(int[] a, @Positive int y) {
@LTLengthOf("a") int x = a.length - 1;
int z = x - y;
a[z + y] = 0;
}
}
|
