File: LTLengthOfPostcondition.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 22,840 kB
  • sloc: java: 145,910; xml: 839; sh: 518; makefile: 401; perl: 26
file content (46 lines) | stat: -rw-r--r-- 1,360 bytes parent folder | download | duplicates (3)
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);
        }
    }
}