package Examples;

import Sequenic.T2.T2annotation.IntRange;

public class PreTest {
	private int x = 0;
	
	//@IntRange(min = x+1, max = 5) // can't use something like this cause x is not a constant
	public void m1(int i) {
		assert(i != x) : "PRE";
		
		if(i == x) {
			throw new Error("i can't be "+x);
		}
	}
	
	public void m2() {
		m1(x); // This is a bug, but it's not caught by T2 cause of the PRE condition in m1
	}
	
	// If you would remove 0 completely from the basedomain it wouldn't be able to cover m3 anymore
	public void m3(int i) {
		assert(i == x) : "PRE";
		
		if(i != x) {
			throw new Error("i must be "+x);
		}
	}
}