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
37
38
39
40
41
42
43
44
45
46
47
|
import org.checkerframework.checker.index.qual.*;
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;
}
}
|
