From 6fad4313b1a4e7f8e6cfcd12b92126a3d9ad58d0 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 4 Jan 2016 19:26:36 -0800
Subject: Added several test cases and some basic documentation for fp usage

---
 float_test19.bpl | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 float_test19.bpl

(limited to 'float_test19.bpl')

diff --git a/float_test19.bpl b/float_test19.bpl
new file mode 100644
index 00000000..f00d8a2b
--- /dev/null
+++ b/float_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
-- 
cgit v1.2.3