| import org.checkerframework.checker.index.qual.HasSubsequence; |
| import org.checkerframework.checker.index.qual.IndexFor; |
| import org.checkerframework.checker.index.qual.IndexOrHigh; |
| |
| public class BasicSubsequence2 { |
| @HasSubsequence(subsequence = "this", from = "this.start", to = "this.end") |
| int[] array; |
| |
| @HasSubsequence(subsequence = "this", from = "start", to = "end") |
| int[] array2; |
| |
| final @IndexFor("array") int start; |
| |
| final @IndexOrHigh("array") int end; |
| |
| private BasicSubsequence2(@IndexFor("array") int s, @IndexOrHigh("array") int e) { |
| start = s; |
| end = e; |
| } |
| |
| void testStartIndex(@IndexFor("this") int x) { |
| @IndexFor("array") int y = x + start; |
| } |
| |
| void testViewpointAdaption(@IndexFor("this") int x) { |
| @IndexFor("array2") int y = x + start; |
| } |
| |
| void testArrayAccess(@IndexFor("this") int x) { |
| int y = array[x + start]; |
| } |
| |
| void testCommutativity(@IndexFor("this") int x) { |
| @IndexFor("array") int y = start + x; |
| } |
| } |