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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
import org.checkerframework.checker.index.qual.*;
import org.checkerframework.common.value.qual.*;
class BinomialTest {
static final long @MinLen(1) [] factorials = {1L, 1L, 1L * 2};
public static long binomial(
@NonNegative @LTLengthOf("this.factorials") int n,
@NonNegative @LessThan("#1 + 1") int k) {
return factorials[k];
}
public static void binomial0(@LTLengthOf("this.factorials") int n, @LessThan("#1") int k) {
@LTLengthOf(value = "factorials", offset = "1") int i = k;
}
public static void binomial0Error(@LTLengthOf("this.factorials") int n, @LessThan("#1") int k) {
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = "factorials", offset = "2") int i = k;
}
public static void binomial0Weak(@LTLengthOf("this.factorials") int n, @LessThan("#1") int k) {
@LTLengthOf("factorials") int i = k;
}
public static void binomial1(@LTLengthOf("this.factorials") int n, @LessThan("#1 + 1") int k) {
@LTLengthOf("factorials") int i = k;
}
public static void binomial1Error(
@LTLengthOf("this.factorials") int n, @LessThan("#1 + 1") int k) {
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = "factorials", offset = "1") int i = k;
}
public static void binomial2(@LTLengthOf("this.factorials") int n, @LessThan("#1 + 2") int k) {
@LTLengthOf(value = "factorials", offset = "-1") int i = k;
}
public static void binomial2Error(
@LTLengthOf("this.factorials") int n, @LessThan("#1 + 2") int k) {
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = "factorials", offset = "0") int i = k;
}
public static void binomial_1(@LTLengthOf("this.factorials") int n, @LessThan("#1 - 1") int k) {
@LTLengthOf(value = "factorials", offset = "2") int i = k;
}
public static void binomial_1Error(
@LTLengthOf("this.factorials") int n, @LessThan("#1 - 1") int k) {
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = "factorials", offset = "3") int i = k;
}
public static void binomial_2(@LTLengthOf("this.factorials") int n, @LessThan("#1 - 2") int k) {
@LTLengthOf(value = "factorials", offset = "3") int i = k;
}
public static void binomial_2Error(
@LTLengthOf("this.factorials") int n, @LessThan("#1 - 2") int k) {
// :: error: (assignment.type.incompatible)
@LTLengthOf(value = "factorials", offset = "4") int i = k;
}
}
|
