| import org.checkerframework.checker.index.qual.*; |
| |
| public class BasicSubsequence { |
| // :: error: not.final |
| @HasSubsequence(subsequence = "this", from = "this.x", to = "this.y") |
| int[] b; |
| |
| int x; |
| int y; |
| |
| void test2(@NonNegative @LessThan("y + 1") int x1, int[] a) { |
| x = x1; |
| // :: error: to.not.ltel |
| b = a; |
| } |
| |
| void test3(@NonNegative @LessThan("y") int x1, int[] a) { |
| x = x1; |
| // :: error: to.not.ltel |
| b = a; |
| } |
| |
| void test4(@NonNegative int x1, int[] a) { |
| x = x1; |
| // :: error: from.gt.to :: error: to.not.ltel |
| b = a; |
| } |
| |
| void test5(@GTENegativeOne @LessThan("y + 1") int x1, int[] a) { |
| x = x1; |
| // :: error: from.not.nonnegative :: error: to.not.ltel |
| b = a; |
| } |
| |
| void test6(@GTENegativeOne int x1, int[] a) { |
| x = x1; |
| // :: error: from.not.nonnegative :: error: to.not.ltel :: error: from.gt.to |
| b = a; |
| } |
| |
| void test7(@IndexFor("this") @LessThan("y") int x1, @IndexOrHigh("this") int y1, int[] a) { |
| x = x1; |
| y = y1; |
| // :: warning: which.subsequence |
| b = a; |
| } |
| } |