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;
    }
}