| import org.checkerframework.checker.index.qual.IndexFor; |
| import org.checkerframework.checker.index.qual.IndexOrHigh; |
| import org.checkerframework.common.value.qual.MinLen; |
| |
| public class MinLenIndexFor { |
| int @MinLen(2) [] arrayLen2 = {0, 1, 2}; |
| |
| void test(@IndexFor("this.arrayLen2") int i) { |
| int j = arrayLen2[i]; |
| int j2 = arrayLen2[1]; |
| } |
| |
| void callTest(int x) { |
| test(0); |
| test(1); |
| // :: error: (argument) |
| test(2); |
| // :: error: (argument) |
| test(3); |
| test(arrayLen2.length - 1); |
| } |
| |
| int @MinLen(4) [] arrayLen4 = {0, 1, 2, 4, 5}; |
| |
| void test2(@IndexOrHigh("this.arrayLen4") int i) { |
| if (i > 0) { |
| int j = arrayLen4[i - 1]; |
| } |
| int j2 = arrayLen4[1]; |
| } |
| |
| void callTest2(int x) { |
| test2(0); |
| test2(1); |
| test2(2); |
| test2(4); |
| // :: error: (argument) |
| test2(5); |
| test2(arrayLen4.length); |
| } |
| } |