package Examples;

import Sequenic.T2.T2annotation.IntRange;

public class SimpleLoops {
	@IntRange(min = -5, max = 15)
	public int methodWithLoop(int x) {
		while (x < 10)
			x++;
		return x;
	}
	
	@IntRange(min = -5, max = 15)
	public int methodWithRepeat(int x) {
		do {
			x++;
		} while (x < 10);
		return x;
	}
	
	// 1 unfeasible path here
	@IntRange(min = -5, max = 15)
	public int methodWithLoopAndIf(int x) {
		int y = 0;
		while (x < 10) {
			x++;
			// require x<=3 to reach the "then" part
			if (x < 5)
				y++;
			else
				y = 0;
		}
		return x;
	}
	
	@IntRange(min = -5, max = 15)
	public int methodWithNestedLoop(int x) {
		while (x < 10) {
			x++;
			// 2 unfeasible paths because of this:
			int y = 10;
			while (y > 0)
				y--;
		}
		return x;
	}
}