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
67
68
69
70
71
72
73
74
75
|
import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.PolyLowerBound;
import org.checkerframework.checker.index.qual.PolySameLen;
import org.checkerframework.checker.index.qual.PolyUpperBound;
import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.checker.index.qual.SameLen;
class Polymorphic {
// Identity functions
@PolyLowerBound int lbc_identity(@PolyLowerBound int a) {
return a;
}
int @PolySameLen [] samelen_identity(int @PolySameLen [] a) {
int @SameLen("a") [] x = a;
return a;
}
@PolyUpperBound int ubc_identity(@PolyUpperBound int a) {
return a;
}
// SameLen tests
void samelen_id(int @SameLen("#2") [] a, int[] a2) {
int[] banana;
int @SameLen("a2") [] b = samelen_identity(a);
// :: error: (assignment.type.incompatible)
int @SameLen("banana") [] c = samelen_identity(b);
}
// UpperBound tests
void ubc_id(
int[] a,
int[] b,
@LTLengthOf("#1") int ai,
@LTEqLengthOf("#1") int al,
@LTLengthOf({"#1", "#2"}) int abi,
@LTEqLengthOf({"#1", "#2"}) int abl) {
int[] c;
@LTLengthOf("a") int ai1 = ubc_identity(ai);
// :: error: (assignment.type.incompatible)
@LTLengthOf("b") int ai2 = ubc_identity(ai);
@LTEqLengthOf("a") int al1 = ubc_identity(al);
// :: error: (assignment.type.incompatible)
@LTLengthOf("a") int al2 = ubc_identity(al);
@LTLengthOf({"a", "b"}) int abi1 = ubc_identity(abi);
// :: error: (assignment.type.incompatible)
@LTLengthOf({"a", "b", "c"}) int abi2 = ubc_identity(abi);
@LTEqLengthOf({"a", "b"}) int abl1 = ubc_identity(abl);
// :: error: (assignment.type.incompatible)
@LTEqLengthOf({"a", "b", "c"}) int abl2 = ubc_identity(abl);
}
// LowerBound tests
void lbc_id(@NonNegative int n, @Positive int p, @GTENegativeOne int g) {
@NonNegative int an = lbc_identity(n);
// :: error: (assignment.type.incompatible)
@Positive int bn = lbc_identity(n);
@GTENegativeOne int ag = lbc_identity(g);
// :: error: (assignment.type.incompatible)
@NonNegative int bg = lbc_identity(g);
@Positive int ap = lbc_identity(p);
}
}
|
