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
|
// Test case for kelloggm 218
// https://github.com/kelloggm/checker-framework/issues/218
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;
public class Modulo {
void m1(Object[] a, @IndexOrHigh("#1") int i, @NonNegative int j) {
@IndexFor("a") int k = j % i;
}
void m1p(Object[] a, @Positive @LTEqLengthOf("#1") int i, @Positive int j) {
@IndexFor("a") int k = j % i;
}
void m2(Object[] a, int i, @IndexFor("#1") int j) {
@IndexFor("a") int k = j % i;
}
void m2(Object[] a, Object[] b, @IndexFor("#1") int i, @IndexFor("#2") int j) {
@IndexFor({"a", "b"}) int k = j % i;
}
}
|
