Added several test cases and some basic documentation for fp usage

1 files changed, 18 insertions, 3 deletions

diff --git a/float_test10.bpl b/float_test10.bpl
index 7423a3a0..566f7a56 100644
--- a/float_test10.bpl
+++ b/float_test10.bpl
@@ -1,5 +1,20 @@
- procedure F() returns () {
+//Translation from loop.c
+//Should return an error?  (The real case does as well...)
+
+procedure main() returns () {
 	var x : float;
-	x := fp (0.5 23 8);
-	assert x == fp (0 -1);
+	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