| // 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; |
| } |
| } |