| // Test case for Issue panacekcz#12: |
| // https://github.com/panacekcz/checker-framework/issues/12 |
| |
| import org.checkerframework.checker.index.qual.IndexFor; |
| import org.checkerframework.checker.index.qual.IndexOrHigh; |
| import org.checkerframework.checker.index.qual.LTLengthOf; |
| import org.checkerframework.checker.index.qual.LTOMLengthOf; |
| import org.checkerframework.checker.index.qual.NonNegative; |
| import org.checkerframework.common.value.qual.IntVal; |
| |
| public class RefineNeqLength { |
| void refineNeqLength(int[] array, @IndexOrHigh("#1") int i) { |
| // Refines i <= array.length to i < array.length |
| if (i != array.length) { |
| refineNeqLengthMOne(array, i); |
| } |
| // No refinement |
| if (i != array.length - 1) { |
| // :: error: (argument) |
| refineNeqLengthMOne(array, i); |
| } |
| } |
| |
| void refineNeqLengthMOne(int[] array, @IndexFor("#1") int i) { |
| // Refines i < array.length to i < array.length - 1 |
| if (i != array.length - 1) { |
| refineNeqLengthMTwo(array, i); |
| // :: error: (argument) |
| refineNeqLengthMThree(array, i); |
| } |
| } |
| |
| void refineNeqLengthMTwo(int[] array, @NonNegative @LTOMLengthOf("#1") int i) { |
| // Refines i < array.length - 1 to i < array.length - 2 |
| if (i != array.length - 2) { |
| refineNeqLengthMThree(array, i); |
| } |
| // No refinement |
| if (i != array.length - 1) { |
| // :: error: (argument) |
| refineNeqLengthMThree(array, i); |
| } |
| } |
| |
| void refineNeqLengthMTwoNonLiteral( |
| int[] array, |
| @NonNegative @LTOMLengthOf("#1") int i, |
| @IntVal(3) int c3, |
| @IntVal({2, 3}) int c23) { |
| // Refines i < array.length - 1 to i < array.length - 2 |
| if (i != array.length - (5 - c3)) { |
| refineNeqLengthMThree(array, i); |
| } |
| // No refinement |
| if (i != array.length - c23) { |
| // :: error: (argument) |
| refineNeqLengthMThree(array, i); |
| } |
| } |
| |
| @LTLengthOf(value = "#1", offset = "3") int refineNeqLengthMThree( |
| int[] array, @NonNegative @LTLengthOf(value = "#1", offset = "2") int i) { |
| // Refines i < array.length - 2 to i < array.length - 3 |
| if (i != array.length - 3) { |
| return i; |
| } |
| // :: error: (return) |
| return i; |
| } |
| |
| // The same test for a string. |
| @LTLengthOf(value = "#1", offset = "3") int refineNeqLengthMThree( |
| String str, @NonNegative @LTLengthOf(value = "#1", offset = "2") int i) { |
| // Refines i < str.length() - 2 to i < str.length() - 3 |
| if (i != str.length() - 3) { |
| return i; |
| } |
| // :: error: (return) |
| return i; |
| } |
| } |