1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
import org.checkerframework.checker.index.qual.HasSubsequence;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
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;
}
}
|
