framework/tests/value/loops/WidenedUpperBound.java

import java.util.List;
import org.checkerframework.common.value.qual.IntRange;

// Because the analysis of loops isn't precise enough, the Value Checker issues
// warnings on this test case. So, suppress those warnings, but run the tests
// to make sure that dataflow reaches a fixed point.
// The expected errors in comments are the errors that should be issued if dataflow were precise
// enough.
@SuppressWarnings("value")
public class WidenedUpperBound {

  void increment() {
    int forIndex;
    for (forIndex = 0; forIndex < 4323; forIndex++) {
      @IntRange(from = 0, to = 4322) int x = forIndex;
    }
    //// ::error: (assignment)
    @IntRange(from = 0, to = 4322) int x = forIndex;
    @IntRange(from = 4323) int y = forIndex;

    int whileIndex = 0;
    while (whileIndex < 1234) {
      @IntRange(from = 0, to = 1233) int z = whileIndex;
      whileIndex++;
    }
    //// ::error: (assignment)
    @IntRange(from = 0, to = 1233) int a = whileIndex;
    @IntRange(from = 1234) int b = whileIndex;

    int doWhileIndex = 0;
    do {
      @IntRange(from = 0, to = 2344) int c = doWhileIndex;
      doWhileIndex++;
    } while (doWhileIndex < 2345);
    //// ::error: (assignment)
    @IntRange(from = 0, to = 2344) int d = doWhileIndex;
    @IntRange(from = 2345) int e = doWhileIndex;
  }

  void decrement() {
    int forIndex;
    for (forIndex = 4323; forIndex > 0; forIndex--) {
      @IntRange(from = 1, to = 4323) int x = forIndex;
    }
    //// ::error: (assignment)
    @IntRange(from = 1, to = 4323) int x = forIndex;
    @IntRange(to = 0) int y = forIndex;

    int whileIndex = 1234;
    while (whileIndex > 0) {
      @IntRange(from = 1, to = 1234) int z = whileIndex;
      whileIndex--;
    }
    //// ::error: (assignment)
    @IntRange(from = 1, to = 1234) int a = whileIndex;
    @IntRange(to = 0) int b = whileIndex;

    int doWhileIndex = 2344;
    do {
      @IntRange(from = 1, to = 2344) int c = doWhileIndex;
      doWhileIndex--;
    } while (doWhileIndex > 0);
    //// ::error: (assignment)
    @IntRange(from = 1, to = 2344) int d = doWhileIndex;
    @IntRange(to = 0) int e = doWhileIndex;
  }

  static void test1() {
    for (int i = 40; i > 0; i--) {
      @IntRange(from = 1, to = 40) int x = i;
    }
  }

  static void test1Explicit() {
    for (@IntRange(from = 1, to = 40) int i = 40; i > 0; i--) {
      @IntRange(from = 1, to = 40) int x = i;
    }
  }

  static void test2() {
    for (int i = 0; i < 18; i++) {
      @IntRange(from = 0, to = 17) int x = i;
    }
  }

  static void test2Explicit() {
    for (@IntRange(from = 0, to = 17) int i = 0; i < 18; i++) {
      @IntRange(from = 0, to = 17) int x = i;
    }
  }

  static void test3() {
    for (int i = 0; i < 18; i++) {
      @IntRange(from = 0, to = 17) int x = i;
    }
  }

  static void evenOdd(int param) {
    for (int i = 0; i < 12; i++) {
      if (i % 2 == 0) {
        @IntRange(from = 0, to = 11) int z = i;
      }
      @IntRange(from = 0, to = 11) int x = i;
    }

    for (int i = 0; i < 12; i++) {
      if (param == 0) {
        @IntRange(from = 0, to = 11) int z = i;
      }
      @IntRange(from = 0, to = 11) int x = i;
    }
  }

  static void evenOdd2(int param) {
    for (int i = 0; i < 300; i++) {
      if (i % 2 == 0) {
        @IntRange(from = 0, to = 299) int z = i;
      }
      @IntRange(from = 0, to = 299) int x = i;
    }

    for (int i = 0; i < 399; i++) {
      if (param == 0) {
        @IntRange(from = 0, to = 398) int z = i;
      }
      @IntRange(from = 0, to = 398) int x = i;
    }
  }

  void ifBlock(int param) {
    int x = 10;
    if (x < param) {
      x = param;
    }
    int z = 40;
    if (z < param) {
      param = 40;
    }
  }

  void doWhile() {
    int d = 0;
    do {
      @IntRange(from = 0, to = 399) int x = d;
      if (d % 2 == 0) {
        @IntRange(from = 0, to = 399) int y = d;
      }

      d++;
    } while (d < 399);

    @IntRange(from = 399) int z = d;
  }

  void doWhileMax() {
    int d = 0;
    do {
      @IntRange(from = 0) int x = d;
      if (d % 2 == 0) {
        @IntRange(from = 0) int y = d;
      }

      d++;
    } while (d < Integer.MAX_VALUE);

    @IntRange(from = 399) int z = d;
  }

  void whileLoop() {
    int i = 0;
    while (i < 399) {
      @IntRange(from = 0, to = 399) int x = i;
      if (i % 2 == 0) {
        @IntRange(from = 0, to = 399) int y = i;
      }

      i++;
    }

    @IntRange(from = 399) int z = i;
  }

  static void testMax() {
    for (int i = 0; i < Integer.MAX_VALUE; i++) {
      @IntRange(from = 0, to = Integer.MAX_VALUE - 1) int x = i;
    }
  }

  void exceptionLoop(List<Object> list) {
    int x = 0;
    for (short z = 0; z < list.size(); z++) {
      x = z;
      if (z == 100) {
        break;
      }
    }
    @IntRange(from = 0, to = 127) int result = x;
  }
}