Polished up the floats test folder. Preparing to rebase

13 files changed, 4 insertions, 298 deletions

diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect
index 19e55fef..9365da58 100644
--- a/Test/floats/float11.bpl.expect
+++ b/Test/floats/float11.bpl.expect
@@ -1,7 +1,7 @@
-..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold.

+float11.bpl(21,2): Error BP5001: This assertion might not hold.

 Execution trace:

-    ..\Test\floats\float11.bpl(12,7): anon0

-    ..\Test\floats\float11.bpl(16,2): anon3_LoopHead

-    ..\Test\floats\float11.bpl(16,2): anon3_LoopDone

+    float11.bpl(12,7): anon0

+    float11.bpl(16,2): anon3_LoopHead

+    float11.bpl(16,2): anon3_LoopDone

 

 Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
deleted file mode 100644
index 4fe25140..00000000
--- a/Test/floats/float13.bpl
+++ /dev/null
@@ -1,23 +0,0 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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 : float64;
-
-	havoc x;
-	assume(x >= TO_FLOAT64_INT(0) && x <= TO_FLOAT64_INT(10));
-
-	y := x*x - x;
-	if (y >= TO_FLOAT64_INT(0)) {
-		y := x / TO_FLOAT64_INT(10);
-	}
-	else {
-		y := x*x + TO_FLOAT64_INT(2);
-	}
-	
-	assert(y >= TO_FLOAT64_INT(0) && y <= TO_FLOAT64_INT(105));
-}
\ No newline at end of file
diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl
deleted file mode 100644
index 46c1b07d..00000000
--- a/Test/floats/float14.bpl
+++ /dev/null
@@ -1,17 +0,0 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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 : float64;
-	var r : float64;
-	
-	x := TO_FLOAT64_INT(77617);
-	y := TO_FLOAT64_INT(33096);
-	r := y*y*y*y*y*y * TO_FLOAT64_REAL(333.75) + x*x * (x*x*y*y*TO_FLOAT64_INT(11) - y*y*y*y*y*y - y*y*y*y * TO_FLOAT64_INT(121) - TO_FLOAT64_INT(2)) + y*y*y*y*y*y*y*y * TO_FLOAT64_REAL(5.5) + x / (y*TO_FLOAT64_INT(2));
-	
-	assert(r >= TO_FLOAT64_INT(0));
-}
\ No newline at end of file
diff --git a/Test/floats/float15.bpl b/Test/floats/float15.bpl
deleted file mode 100644
index 7536f8fd..00000000
--- a/Test/floats/float15.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//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/float16.bpl b/Test/floats/float16.bpl
deleted file mode 100644
index 6bef1137..00000000
--- a/Test/floats/float16.bpl
+++ /dev/null
@@ -1,40 +0,0 @@
-//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/float17.bpl b/Test/floats/float17.bpl
deleted file mode 100644
index 8e07878d..00000000
--- a/Test/floats/float17.bpl
+++ /dev/null
@@ -1,38 +0,0 @@
-//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/float18.bpl b/Test/floats/float18.bpl
deleted file mode 100644
index 7e78e206..00000000
--- a/Test/floats/float18.bpl
+++ /dev/null
@@ -1,16 +0,0 @@
-//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/float19.bpl b/Test/floats/float19.bpl
deleted file mode 100644
index c3a42e6b..00000000
--- a/Test/floats/float19.bpl
+++ /dev/null
@@ -1,34 +0,0 @@
-//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
diff --git a/Test/floats/float20.bpl b/Test/floats/float20.bpl
deleted file mode 100644
index 57c605fd..00000000
--- a/Test/floats/float20.bpl
+++ /dev/null
@@ -1,14 +0,0 @@
-//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/float21.bpl b/Test/floats/float21.bpl
deleted file mode 100644
index 5fad5859..00000000
--- a/Test/floats/float21.bpl
+++ /dev/null
@@ -1,35 +0,0 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-

-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_INT(0)) {

-		y := x * x;

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

-		z := TO_FLOAT32_INT(1) / y;

-	}

-}

-

-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/float22.bpl b/Test/floats/float22.bpl
deleted file mode 100644
index 1505c361..00000000
--- a/Test/floats/float22.bpl
+++ /dev/null
@@ -1,20 +0,0 @@
-//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/float23.bpl b/Test/floats/float23.bpl
deleted file mode 100644
index 69ae243d..00000000
--- a/Test/floats/float23.bpl
+++ /dev/null
@@ -1,8 +0,0 @@
-//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/modpath.py b/Test/floats/modpath.py
deleted file mode 100644
index 90707701..00000000
--- a/Test/floats/modpath.py
+++ /dev/null
@@ -1,13 +0,0 @@
-import sys

-

-f = open(sys.argv[1], 'r')

-to_write = ""

-

-for i in f:

-	to_write += i.replace("..\\Test\\floats\\", "")

-	

-f.close()

-

-f = open(sys.argv[1], 'w')

-

-f.write(to_write)
\ No newline at end of file