framework/tests/value/loops/OscillatingLoops.java

import org.checkerframework.common.value.qual.IntRange;
import org.checkerframework.common.value.qual.IntVal;

// 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.
@SuppressWarnings("value")
public class OscillatingLoops {

  void oscillatesDoWhile() {
    int i = 0;
    int d = 0;
    do {
      i++;
      if (d > 4566) {
        d = 0;
      } else {
        d++;
      }
    } while (i < Integer.MAX_VALUE);
    @IntRange(from = 0, to = 4567) int after = d;
    @IntVal(Integer.MAX_VALUE) int afterI = i;
  }

  void oscillatesWhile() {
    int i = 0;
    int d = 1;
    while (i < Integer.MAX_VALUE) {
      i++;
      if (d > 4566) {
        d = 0;
      } else {
        d++;
      }
    }
    @IntRange(from = 0, to = 4567) int after = d;
    @IntVal(Integer.MAX_VALUE) int afterI = i;
  }

  void oscillatesDoWhile2() {
    int i = 0;
    int d = 0;
    do {
      if (d > 4566) {
        d = 0;
      } else {
        d++;
      }
      i++;
    } while (i < Integer.MAX_VALUE);
    @IntRange(from = -128, to = 32767) int after = d;
    @IntVal(Integer.MAX_VALUE) int afterI = i;
  }

  void oscillatesFor() {
    int d = 0;
    for (int i = 0; i < Integer.MAX_VALUE; i++) {
      if (d > 4566) {
        d = 0;
      } else {
        d++;
      }
    }
    @IntRange(from = -128, to = 32767) int after = d;
  }
}