moved all the tests to the testing folder

20 files changed, 525 insertions, 0 deletions

diff --git a/Test/floats/test1.bpl b/Test/floats/test1.bpl
new file mode 100644
index 00000000..e893e098
--- /dev/null
+++ b/Test/floats/test1.bpl
@@ -0,0 +1,13 @@
+//Translation from addsub_double_exact.c
+//Should Verify
+procedure main() returns () {
+	var x : float<11, 53>;
+	var y : float<11, 53>;
+	var z : float<11, 53>;
+	var r : float<11, 53>;
+	x := fp<11, 53> (10000000bv64);
+	y := x + fp<11, 53>(1bv64);
+	z := x - fp<11, 53>(1bv64);
+	r := y - z;
+	assert r == fp<11, 53> (2bv64);
+}
\ No newline at end of file
diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl
new file mode 100644
index 00000000..566f7a56
--- /dev/null
+++ b/Test/floats/test10.bpl
@@ -0,0 +1,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));
+}
\ No newline at end of file
diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl
new file mode 100644
index 00000000..cee3e36e
--- /dev/null
+++ b/Test/floats/test11.bpl
@@ -0,0 +1,55 @@
+//Translation from interpolation.c

+//Should Verify

+//Returns inconclusive?  What does that mean?

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+procedure main() returns () {

+	var i : int;

+	var z : float32;

+	var t : float32;

+	var min : [int] float32;

+	var max : [int] float32;

+	

+	min[0] := TO_FLOAT32_INT(5);

+	min[1] := TO_FLOAT32_INT(10);

+	min[2] := TO_FLOAT32_INT(12);

+	min[3] := TO_FLOAT32_INT(30);

+	min[4] := TO_FLOAT32_INT(150);

+	

+	max[0] := TO_FLOAT32_INT(10);

+	max[1] := TO_FLOAT32_INT(12);

+	max[2] := TO_FLOAT32_INT(30);

+	max[3] := TO_FLOAT32_INT(150);

+	max[4] := TO_FLOAT32_INT(300);

+	

+	havoc t;

+	assume(t >= min[0] && t <= max[4]);

+	

+	i := 0;

+	//while (i < 5) {

+		//if (t <= max[i]) {

+			//break;

+		//}

+		//i := i + 1;

+	//}

+	

+	if (t > max[0]) { //1

+		i := i + 1;

+	}

+	if (t > max[1]) { //2

+		i := i + 1;

+	}

+	if (t > max[2]) { //3

+		i := i + 1;

+	}

+	if (t > max[3]) { //4

+		i := i + 1;

+	}

+	if (t > max[4]) { //5

+		i := i + 1;

+	}

+	

+	z := (t - min[i]) / (max[i] - min[i]);

+	

+	assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));

+}
\ No newline at end of file
diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl
new file mode 100644
index 00000000..c733b9f4
--- /dev/null
+++ b/Test/floats/test12.bpl
@@ -0,0 +1,43 @@
+//Translation from inv_Newton.c

+//Should Verify

+//Unfinished code!

+

+procedure inv(float(11 53)) returns(float(11 53)) {

+	var z : float(11 53);

+	var t : float(11 53);

+	var t : float(11 53);

+	

+	

+}

+

+procedure main() returns () {

+	var t : float(11 53);

+	var t : float(11 53);

+	

+	min[0] := fp(5);

+	min[1] := fp(10);

+	min[2] := fp(12);

+	min[3] := fp(30);

+	min[4] := fp(150);

+	

+	max[0] := fp(10);

+	max[1] := fp(12);

+	max[2] := fp(30);

+	max[3] := fp(150);

+	max[4] := fp(300);

+	

+	havoc t;

+	assume(t >= min[0] && t <= max[4]);

+	

+	i := 0;

+	while (i < 5) {

+		if (t <= max[i]) {

+			break;

+		}

+		i := i + 1;

+	}

+	

+	z := (t - min[i]) / (max[i] - min[i]);

+	

+	assert(z >= fp(0) && z <= fp(1));

+}
\ No newline at end of file
diff --git a/Test/floats/test13.bpl b/Test/floats/test13.bpl
new file mode 100644
index 00000000..e5402539
--- /dev/null
+++ b/Test/floats/test13.bpl
@@ -0,0 +1,19 @@
+//Translation from inv_square_false-unreach-call.c

+//Should return an error (without crashing)

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	

+	havoc x;

+	assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));

+	

+	if (x != TO_FLOAT32_INT(0)) {

+		y := x * x;

+		assert(y != TO_FLOAT32_INT(0));

+		z := TO_FLOAT32_INT(1) / y;

+	}

+}
\ No newline at end of file
diff --git a/Test/floats/test14.bpl b/Test/floats/test14.bpl
new file mode 100644
index 00000000..1505c361
--- /dev/null
+++ b/Test/floats/test14.bpl
@@ -0,0 +1,20 @@
+//Translation from inv_square_true-unreach-call.c

+//Should Verify

+

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);

+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);

+

+procedure main() returns () {

+	var x : float32;

+	var y : float32;

+	var z : float32;

+	

+	havoc x;

+	assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));

+	

+	if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) {

+		y := x * x;

+		assert(y != TO_FLOAT32_INT(0));

+		z := TO_FLOAT32_INT(1) / y;

+	}

+}
\ No newline at end of file
diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl
new file mode 100644
index 00000000..1dc549ac
--- /dev/null
+++ b/Test/floats/test15.bpl
@@ -0,0 +1,24 @@
+//Translation from Muller_Kahan.c

+//Should Verify

+//NOTE:  (fp(....)) causes a compiler error!

+//FAILS!  Heavily...

+

+procedure main() returns () {

+	var x0 : float(11 53);

+	var x1 : float(11 53);

+	var x2 : float(11 53);

+	var i : int;

+	

+	x0 := fp(11 11 53) / fp(2 11 53);

+	x1 := fp(61 11 53) / fp(11 11 53);

+	i := 0;

+	while (i < 100) {

+		x2 := fp(1130 11 53) - fp(3000 11 53) / x0;

+		x2 := fp(111 11 53) - x2 / x1;

+		x0 := x1;

+		x1 := x2;

+		i := i + 1;

+	}

+	

+	assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53));

+}
\ No newline at end of file
diff --git a/Test/floats/test16.bpl b/Test/floats/test16.bpl
new file mode 100644
index 00000000..69ae243d
--- /dev/null
+++ b/Test/floats/test16.bpl
@@ -0,0 +1,8 @@
+//Translation from nan_double_false-unreach-call.c

+//Should return an error

+

+procedure main() returns () {

+	var x : float(11 53);

+	havoc x;

+	assert(x==x);

+}
\ No newline at end of file
diff --git a/Test/floats/test17.bpl b/Test/floats/test17.bpl
new file mode 100644
index 00000000..caa1fa74
--- /dev/null
+++ b/Test/floats/test17.bpl
@@ -0,0 +1,11 @@
+//Translation from nan_double_range_true-unreach-call.c

+//Should verify

+//Uggghhhh, should I add support for e?

+

+procedure main() returns () {

+	var x : float(11 53);

+	havoc x;

+	if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) {	

+		assert(x==x);

+	}

+}
\ No newline at end of file
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl
new file mode 100644
index 00000000..71eb5286
--- /dev/null
+++ b/Test/floats/test18.bpl
@@ -0,0 +1,36 @@
+//Translation from rlim_exit.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;

+		}

+		

+		i := i + 1;

+	}

+	

+	assert(Y >= fp(-129) && Y <= fp(129));

+}
\ No newline at end of file
diff --git a/Test/floats/test19.bpl b/Test/floats/test19.bpl
new file mode 100644
index 00000000..f00d8a2b
--- /dev/null
+++ b/Test/floats/test19.bpl
@@ -0,0 +1,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;

+	}

+}
\ No newline at end of file
diff --git a/Test/floats/test2.bpl b/Test/floats/test2.bpl
new file mode 100644
index 00000000..d78c339d
--- /dev/null
+++ b/Test/floats/test2.bpl
@@ -0,0 +1,17 @@
+//Translation from addsub_float_exact.c
+//Should Verify
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
+
+procedure main() returns () {
+	var x : float32;
+	var y : float32;
+	var z : float32;
+	var r : float32;
+	x := TO_FLOAT32_REAL(1e7);
+	y := x + TO_FLOAT32_INT(1);
+	z := x - TO_FLOAT32_INT(1);
+	r := y - z;
+	assert r == TO_FLOAT32_INT(2);
+}
\ No newline at end of file
diff --git a/Test/floats/test20.bpl b/Test/floats/test20.bpl
new file mode 100644
index 00000000..57c605fd
--- /dev/null
+++ b/Test/floats/test20.bpl
@@ -0,0 +1,14 @@
+//Should return an error?

+//Translation from Rump_double.c

+

+procedure main() returns () {

+	var x : float(11 53);

+	var y : float(11 53);

+	var r : float(11 53);

+	

+	x := fp(77617 11 53);

+	y := fp(33096 11 53);

+	r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53));

+	

+	assert(r >= fp(0 11 53));

+}
\ No newline at end of file
diff --git a/Test/floats/test3.bpl b/Test/floats/test3.bpl
new file mode 100644
index 00000000..67c6ba48
--- /dev/null
+++ b/Test/floats/test3.bpl
@@ -0,0 +1,13 @@
+//Translation from addsub_float_inexact.c
+//Should give an error
+procedure main() returns () {
+	var x : float32;
+	var y : float32;
+	var z : float32;
+	var r : float32;
+	x := fp<8, 24>(3221225472bv32);
+	y := x + fp<8, 24>(1bv32);
+	z := x - fp<8, 24>(1bv32);
+	r := y - z;
+	assert r == fp<8, 24>(2bv32);
+}
\ No newline at end of file
diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl
new file mode 100644
index 00000000..a31aa215
--- /dev/null
+++ b/Test/floats/test4.bpl
@@ -0,0 +1,32 @@
+//Translation from drift_tenth.c
+//Should Fail
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
+
+procedure main() returns () {
+	var tick : float32;
+	var time : float32;
+	var i: int;
+	
+	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+	time := TO_FLOAT32_INT(0);
+	
+	//i := 0;
+	//while (i < 10)
+	//{
+	//	time := time + tick;
+	//	i := i + 1;
+	//}
+	time := time + tick;//1
+	time := time + tick;//2
+	time := time + tick;//3
+	time := time + tick;//4
+	time := time + tick;//5
+	time := time + tick;//6
+	time := time + tick;//7
+	time := time + tick;//8
+	time := time + tick;//9
+	time := time + tick;//10
+	assert time == TO_FLOAT32_INT(1);
+}
\ No newline at end of file
diff --git a/Test/floats/test5.bpl b/Test/floats/test5.bpl
new file mode 100644
index 00000000..7536f8fd
--- /dev/null
+++ b/Test/floats/test5.bpl
@@ -0,0 +1,36 @@
+//Translation from filter1.c
+//Should Verify
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure main() returns () {
+	var E0 : float64;
+	var E1 : float64;
+	var S : float64);
+	var i : int;
+	var rand : int;
+	
+	E1 := TO_FLOAT64_INT(0);
+	S := TO_FLOAT64_INT(0);
+	
+	i := 0;
+	while (i <= 1000000)
+	{
+		havoc E0;
+		assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53));
+		
+		havoc rand;
+		if (rand != 0) {
+			S := fp(0 11 53);
+		}
+		else {
+			S := fp(0.999 11 53) * S + E0 - E1;
+		}
+		E1 := E0;
+		
+		//assert(1==0);
+		assert(S >= fp(-1 11 53) && S <= fp(1 11 53));
+		i := i + 1;
+	}
+}
\ No newline at end of file
diff --git a/Test/floats/test6.bpl b/Test/floats/test6.bpl
new file mode 100644
index 00000000..6bef1137
--- /dev/null
+++ b/Test/floats/test6.bpl
@@ -0,0 +1,40 @@
+//Translation from filter2.c
+//Should give an error
+//FAILS; doesn't generate terms!
+
+procedure main() returns () {
+	var E : float(11 53);
+	var E0 : float(11 53);
+	var E1 : float(11 53);
+	var S : float(11 53);
+	var S0 : float(11 53);
+	var S1 : float(11 53);
+	var i: int;
+	
+	havoc E;
+	havoc E0;
+	assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53));
+	assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53));
+	
+	E1 := fp(0.0 11 53);
+	S1 := fp(0.0 11 53);
+	S0 := fp(0.0 11 53);
+	S := fp(0.0 11 53);
+	
+	i := 0;
+//	while (i <= 1000000)
+//	{
+		E1 := E0;
+		E0 := E;
+	
+		havoc E;
+		assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53));
+		
+		S1 := S0;
+		S0 := S;
+		S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53);
+		
+		assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53));
+		//i := i + 1;
+//	}
+}
\ No newline at end of file
diff --git a/Test/floats/test7.bpl b/Test/floats/test7.bpl
new file mode 100644
index 00000000..8e07878d
--- /dev/null
+++ b/Test/floats/test7.bpl
@@ -0,0 +1,38 @@
+//Translation from filter2.c
+//Should give an error
+//Same as the previous one; it works with reals!
+
+procedure main() returns () {
+	var E : real;
+	var E0 : real;
+	var E1 : real;
+	var S : real;
+	var S0 : real;
+	var S1 : real;
+	var i: int;
+	
+	havoc E;
+	havoc E0;
+	assume(E >= 0.0 && E <= 1.0);
+	assume(E0 >= 0.0 && E0 <= 1.0);
+	
+	S0 := 0.0;
+	S := 0.0;
+	
+	i := 0;
+	while (i <= 1000000)
+	{
+		E1 := E0;
+		E0 := E;
+		
+		havoc E;
+		assume(E >= 0.0 && E <= 1.0);
+		
+		S1 := S0;
+		S0 := S;
+		S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7;
+		
+		assert(S >= -4.0 && S <= 4.0);
+		i := i + 1;
+	}
+}
\ No newline at end of file
diff --git a/Test/floats/test8.bpl b/Test/floats/test8.bpl
new file mode 100644
index 00000000..7e78e206
--- /dev/null
+++ b/Test/floats/test8.bpl
@@ -0,0 +1,16 @@
+//Translation from float_double.c
+//Should Verify
+
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+
+procedure main() returns () {
+	var x : float64;
+	var y : float32;
+	
+	x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1);
+	y := TO_FLOAT32_FLOAT64(x);
+	assert x != TO_FLOAT64_FLOAT32(y);
+}
\ No newline at end of file
diff --git a/Test/floats/test9.bpl b/Test/floats/test9.bpl
new file mode 100644
index 00000000..c3a42e6b
--- /dev/null
+++ b/Test/floats/test9.bpl
@@ -0,0 +1,34 @@
+//Translation from feedback_diverge.c
+//Should give an error
+//Not sure on this one...
+
+procedure main() returns () {
+	var A : float;
+	var B : float;
+	var X : float;
+	var i : int;
+	var rand : int;
+	
+	A := fp(0);
+	B := fp(0);
+	
+	i := 0;
+	while (i < 3600000) {
+		
+		havoc rand;
+		if (rand != 0) {
+			havoc X;
+			assume(X >= fp(-20) && X <= fp(20));
+		}
+		else {
+			X := B;
+		}
+		
+		B := B - (B * fp(2.0) - A - X) * fp(.005);
+		A := X;
+		
+		i := i + 1;
+	}
+	
+	assert(A >= fp(-100) && A <= fp(100));
+}
\ No newline at end of file