Test/floats/test10.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

//Translation from loop.c
//Should return an error?  (The real case does as well...)

procedure main() returns () {
	var x : float;
	var y : float;
	var z : float;
	
	x := fp(1);
	y := fp(10000000);
	z := fp(42);
	
	while (x < y) {
		x := x + fp(1);
		y := y - fp(1);
		z := z + fp(1);
	}
	
	assert(z >= fp(0) && z <= fp(10000000));
}