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
|
import java.util.Arrays;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOf;
import org.checkerframework.checker.index.qual.EnsuresLTLengthOfIf;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;
class LTLengthOfPostcondition {
Object[] array;
@NonNegative @LTEqLengthOf("array") int end;
@EnsuresLTLengthOf(value = "end", targetValue = "array", offset = "#1 - 1")
public void shiftIndex(@NonNegative int x) {
int newEnd = end - x;
if (newEnd < 0) throw new RuntimeException();
end = newEnd;
}
public void useShiftIndex(@NonNegative int x) {
// :: error: (argument.type.incompatible)
Arrays.fill(array, end, end + x, null);
shiftIndex(x);
Arrays.fill(array, end, end + x, null);
}
@EnsuresLTLengthOfIf(
expression = "end",
result = true,
targetValue = "array",
offset = "#1 - 1")
public boolean tryShiftIndex(@NonNegative int x) {
int newEnd = end - x;
if (newEnd < 0) {
return false;
}
end = newEnd;
return true;
}
public void useTryShiftIndex(@NonNegative int x) {
if (tryShiftIndex(x)) {
Arrays.fill(array, end, end + x, null);
}
}
}
|