| 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; |
| |
| public 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) |
| 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); |
| } |
| } |
| } |