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
|
import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.LowerBoundUnknown;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;
public class Errors {
void test() {
int[] arr = new int[5];
// unsafe
@GTENegativeOne int n1p = -1;
@LowerBoundUnknown int u = -10;
// safe
@NonNegative int nn = 0;
@Positive int p = 1;
// :: error: (array.access.unsafe.low)
int a = arr[n1p];
// :: error: (array.access.unsafe.low)
int b = arr[u];
int c = arr[nn];
int d = arr[p];
}
}
// a comment
|
