float_test19.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

//Translation from flim_invariant.c
//Should verify
//Unary - unsupported float operations (on my end)...

procedure main() returns () {
	var X : float;
	var Y : float;
	var S : float;
	var R : float;
	var D : float;
	var i : int;
	
	Y := fp(0);
	
	i := 0;
	while (i < 100000) {
		havoc X;
		havoc D;
		assume(X >= fp(-128) && X <= fp(128));
		assume(D >= fp(0) && D <= fp(16));
		
		S := Y;
		Y := X;
		R := X - S;
		if (R <= fp(0)-D) {
			Y := S - D;
		}
		else if(R >= D) {
			Y := S + D;
		}
		
		assert(Y >= fp(-129) && Y <= fp(129));
		
		i := i + 1;
	}
}