File: IndexIntValVsConstant.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (29 lines) | stat: -rw-r--r-- 967 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
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.interning.qual.Interned;
import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.IntVal;

public class IndexIntValVsConstant {

    void m() {

        int @ArrayLen(7) [] a1 = new int[] {1, 2, 3, 4, 5, 6, 7};

        @IntVal(2) int i = 2;
        @IntVal(4) int j = 4;

        int[] s0 = internSubsequence(a1, 2, 4);
        int[] s1 = internSubsequence(a1, i, j);
    }

    int @Interned [] internSubsequence(
            int @Interned [] seq,
            @IndexFor("#1") @LessThan("#3") int start,
            @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int end) {
        // dummy implementation
        return new int[0];
    }
}