From c19c2495497d0dfa7aaf871cf833cd5e5f986d33 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Tue, 31 May 2016 12:59:38 -0600
Subject: moved all the tests to the testing folder

---
 Test/floats/test11.bpl | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 Test/floats/test11.bpl

(limited to 'Test/floats/test11.bpl')

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
-- 
cgit v1.2.3