File: IntroAnd.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 (39 lines) | stat: -rw-r--r-- 1,106 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
import org.checkerframework.checker.index.qual.*;

class IntroAnd {
    void test() {
        @NonNegative int a = 1 & 0;
        @NonNegative int b = a & 5;

        // :: error: (assignment.type.incompatible)
        @Positive int c = a & b;
        @NonNegative int d = a & b;
        @NonNegative int e = b & a;
    }

    void test_ubc_and(
            @IndexFor("#2") int i, int[] a, @LTLengthOf("#2") int j, int k, @NonNegative int m) {
        int x = a[i & k];
        int x1 = a[k & i];
        // :: error: (array.access.unsafe.low) :: error: (array.access.unsafe.high)
        int y = a[j & k];
        if (j > -1) {
            int z = a[j & k];
        }
        // :: error: (array.access.unsafe.high)
        int w = a[m & k];
        if (m < a.length) {
            int u = a[m & k];
        }
    }

    void two_arrays(int[] a, int[] b, @IndexFor("#1") int i, @IndexFor("#2") int j) {
        int l = a[i & j];
        l = b[i & j];
    }

    void test_pos(@Positive int x, @Positive int y) {
        // :: error: (assignment.type.incompatible)
        @Positive int z = x & y;
    }
}