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
|
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.checker.index.qual.NonNegative;
public class Issue2029 {
void lessThanUpperBound(
@NonNegative @LessThan("#2") int index, @NonNegative int size, char val) {
char[] arr = new char[size];
arr[index] = val;
}
void LessThanOffsetLowerBound(
int[] array,
@NonNegative @LTLengthOf("#1") int n,
@NonNegative @LessThan("#2 + 1") int k) {
array[n - k] = 10;
}
void LessThanOffsetUpperBound(
@NonNegative int n,
@NonNegative @LessThan("#1 + 1") int k,
@NonNegative int size,
@NonNegative @LessThan("#3 + 1") int index) {
@NonNegative int m = n - k;
int[] arr = new int[size];
for (; index < arr.length - 1; index++) {
arr[index] = 10;
}
}
}
|
