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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
import java.util.AbstractList;
import java.util.Collections;
import java.util.List;
import org.checkerframework.checker.index.qual.HasSubsequence;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.IndexOrLow;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.common.value.qual.MinLen;
/**
* A simplified version of the Guava primitives classes (such as Bytes, Longs, Shorts, etc.) with
* all expected warnings suppressed.
*/
public class GuavaPrimitives extends AbstractList<Short> {
@HasSubsequence(subsequence = "this", from = "this.start", to = "this.end")
final short @MinLen(1) [] array;
final @IndexFor("array") @LessThan("end") int start;
final @Positive @LTEqLengthOf("array") int end;
public static @IndexOrLow("#1") int indexOf(short[] array, short target) {
return indexOf(array, target, 0, array.length);
}
private static @IndexOrLow("#1") @LessThan("#4") int indexOf(
short[] array, short target, @IndexOrHigh("#1") int start, @IndexOrHigh("#1") int end) {
for (int i = start; i < end; i++) {
if (array[i] == target) {
return i;
}
}
return -1;
}
private static @IndexOrLow("#1") @LessThan("#4") int lastIndexOf(
short[] array, short target, @IndexOrHigh("#1") int start, @IndexOrHigh("#1") int end) {
for (int i = end - 1; i >= start; i--) {
if (array[i] == target) {
return i;
}
}
return -1;
}
GuavaPrimitives(short @MinLen(1) [] array) {
this(array, 0, array.length);
}
@SuppressWarnings(
"index") // these three fields need to be initialized in some order, and any ordering
// leads to the first two issuing errors - since each field is dependent on at
// least one of the others
GuavaPrimitives(
short @MinLen(1) [] array,
@IndexFor("#1") @LessThan("#3") int start,
@Positive @LTEqLengthOf("#1") int end) {
// warnings in here might just need to be suppressed. A single @SuppressWarnings("index") to
// establish rep. invariant might be okay?
this.array = array;
this.start = start;
this.end = end;
}
public @Positive @LTLengthOf(
value = {"this", "array"},
offset = {"-1", "start - 1"}) int
size() { // INDEX: Annotation on a public method refers to private member.
return end - start;
}
public boolean isEmpty() {
return false;
}
public Short get(@IndexFor("this") int index) {
return array[start + index];
}
@SuppressWarnings(
"lowerbound") // https://github.com/kelloggm/checker-framework/issues/227 indexOf()
public @IndexOrLow("this") int indexOf(Object target) {
// Overridden to prevent a ton of boxing
if (target instanceof Short) {
int i = GuavaPrimitives.indexOf(array, (Short) target, start, end);
if (i >= 0) {
return i - start;
}
}
return -1;
}
@SuppressWarnings(
"lowerbound") // https://github.com/kelloggm/checker-framework/issues/227 lastIndexOf()
public @IndexOrLow("this") int lastIndexOf(Object target) {
// Overridden to prevent a ton of boxing
if (target instanceof Short) {
int i = GuavaPrimitives.lastIndexOf(array, (Short) target, start, end);
if (i >= 0) {
return i - start;
}
}
return -1;
}
public Short set(@IndexFor("this") int index, Short element) {
short oldValue = array[start + index];
// checkNotNull for GWT (do not optimize)
array[start + index] = element;
return oldValue;
}
@SuppressWarnings("index") // needs https://github.com/kelloggm/checker-framework/issues/229
public List<Short> subList(
@IndexOrHigh("this") @LessThan("#2") int fromIndex, @IndexOrHigh("this") int toIndex) {
int size = size();
if (fromIndex == toIndex) {
return Collections.emptyList();
}
return new GuavaPrimitives(array, start + fromIndex, start + toIndex);
}
@Override
public String toString() {
StringBuilder builder = new StringBuilder(size() * 6);
builder.append('[').append(array[start]);
for (int i = start + 1; i < end; i++) {
builder.append(", ").append(array[i]);
}
return builder.append(']').toString();
}
}
|
