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 DoWhile {

    void doWhile() {
        int d = 0;
        do {
            d++;
        } while (d < 399);
        @IntRange(from = 399) int after = d;
    }

    void another() {
        int d = 0;
        do {
            d++;
            if (d > 444) {
                break;
            }
            @IntRange(from = 1, to = 444) int z = d;
        } while (true);
    }

    void fromAnno(@IntVal(2222) int param) {
        int d = 0;
        do {
            d++;
            if (d > param) {
                break;
            }
            @IntRange(from = 1, to = 2222) int z = d;
        } while (true);
    }
}