checker/tests/index/IntroAnd.java

import org.checkerframework.checker.index.qual.*;

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

    // :: error: (assignment)
    @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)
    @Positive int z = x & y;
  }
}