From 5cff8cd77c629ec8e48a2498b1e704173306586a Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 21:09:06 -0600
Subject: finished testing, fixed several minor compiler bugs

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

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

diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
new file mode 100644
index 00000000..4fe25140
--- /dev/null
+++ b/Test/floats/float13.bpl
@@ -0,0 +1,23 @@
+// 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
-- 
cgit v1.2.3


From 754f7d3ef36e11740a40a2d687f3b15195f63d9a Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 21:11:23 -0600
Subject: Polished up the floats test folder.  Preparing to rebase

---
 Test/floats/float11.bpl.expect |  8 ++++----
 Test/floats/float13.bpl        | 23 -----------------------
 Test/floats/float14.bpl        | 17 -----------------
 Test/floats/float15.bpl        | 36 ------------------------------------
 Test/floats/float16.bpl        | 40 ----------------------------------------
 Test/floats/float17.bpl        | 38 --------------------------------------
 Test/floats/float18.bpl        | 16 ----------------
 Test/floats/float19.bpl        | 34 ----------------------------------
 Test/floats/float20.bpl        | 14 --------------
 Test/floats/float21.bpl        | 35 -----------------------------------
 Test/floats/float22.bpl        | 20 --------------------
 Test/floats/float23.bpl        |  8 --------
 Test/floats/modpath.py         | 13 -------------
 13 files changed, 4 insertions(+), 298 deletions(-)
 delete mode 100644 Test/floats/float13.bpl
 delete mode 100644 Test/floats/float14.bpl
 delete mode 100644 Test/floats/float15.bpl
 delete mode 100644 Test/floats/float16.bpl
 delete mode 100644 Test/floats/float17.bpl
 delete mode 100644 Test/floats/float18.bpl
 delete mode 100644 Test/floats/float19.bpl
 delete mode 100644 Test/floats/float20.bpl
 delete mode 100644 Test/floats/float21.bpl
 delete mode 100644 Test/floats/float22.bpl
 delete mode 100644 Test/floats/float23.bpl
 delete mode 100644 Test/floats/modpath.py

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

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


From ce9d174eba6a4efd321e78fed4a6e00aab1fda2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Fri, 22 Jul 2016 15:42:33 -0600
Subject: fixed the syntax on former tests and added two fp constant
 translation tests

---
 Test/floats/float1.bpl         | 10 +++++-----
 Test/floats/float13.bpl        | 30 ++++++++++++++++++++++++++++++
 Test/floats/float13.bpl.expect |  2 ++
 Test/floats/float14.bpl        | 22 ++++++++++++++++++++++
 Test/floats/float14.bpl.expect |  9 +++++++++
 Test/floats/float3.bpl         | 18 +++++++++---------
 Test/floats/float4.bpl         | 10 +++++++++-
 Test/floats/float7.bpl         |  8 ++++----
 Test/floats/float8.bpl         |  8 ++++----
 9 files changed, 94 insertions(+), 23 deletions(-)
 create mode 100644 Test/floats/float13.bpl
 create mode 100644 Test/floats/float13.bpl.expect
 create mode 100644 Test/floats/float14.bpl
 create mode 100644 Test/floats/float14.bpl.expect

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

diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl
index 2b901c94..d7fc7837 100644
--- a/Test/floats/float1.bpl
+++ b/Test/floats/float1.bpl
@@ -2,12 +2,12 @@
 // RUN: %diff "%s.expect" "%t"
 procedure foo(x : float24e8) returns (r : float24e8)
 {
-	r := 0e1f24e8;
-	r := 1e0f24e8;
+	r := 0e128f24e8;
+	r := 1e127f24e8;
 	r := x;
-	r := x + 1e0f24e8;
-	r := 0e0f24e8 + 0e0f24e8;
-	assert(r == 0e1f24e8);
+	r := x + 1e127f24e8;
+	r := 0e127f24e8 + 0e127f24e8;
+	assert(r == 0e128f24e8);
 	
 	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
new file mode 100644
index 00000000..9b9fa7cb
--- /dev/null
+++ b/Test/floats/float13.bpl
@@ -0,0 +1,30 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11);
+
+procedure main() returns () {
+	var f : float24e8;
+	var fc : float24e8;
+	var d : float53e11;
+	var dc : float53e11;
+	
+	f := 2097152e129f24e8;
+	fc := TO_FLOAT32_INT(5);
+	assert(f == fc);
+	
+	f := 1048576e128f24e8;
+	fc := TO_FLOAT32_REAL(2.25);
+	assert(f == fc);
+	
+	d := 1125899906842624e1025f53e11;
+	dc := TO_FLOAT64_INT(5);
+	assert(d == dc);
+	
+	d := 562949953421312e1024f53e11;
+	dc := TO_FLOAT64_REAL(2.25);
+	//assert(d == dc);
+}
\ No newline at end of file
diff --git a/Test/floats/float13.bpl.expect b/Test/floats/float13.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/floats/float13.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl
new file mode 100644
index 00000000..1752ef0d
--- /dev/null
+++ b/Test/floats/float14.bpl
@@ -0,0 +1,22 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+	var f : float24e8;
+	var d : float53e11;
+	
+	f := 0e-1f24e8; //Error
+	f := 0e256f24e8; //Error
+	f := 0e255f24e8; //No Error
+	
+	f := 8388608e0f24e8; //Error
+	f := -8388608e0f24e8; //Error
+	f := 8388607e0f24e8; //No Error
+	
+	d := 0e-1f53e11; //Error
+	d := 0e2048f53e11; //Error
+	d := 0e2047f53e11; //No Error
+	
+	d := 4503599627370496e0f53e11; //Error
+	d := -4503599627370496e0f53e11; //Error
+	d := 4503599627370495e0f53e11; //No Error
+}
\ No newline at end of file
diff --git a/Test/floats/float14.bpl.expect b/Test/floats/float14.bpl.expect
new file mode 100644
index 00000000..f42b0286
--- /dev/null
+++ b/Test/floats/float14.bpl.expect
@@ -0,0 +1,9 @@
+float14.bpl(7,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 8
+float14.bpl(8,7): error: incorrectly formatted floating point, The given exponent 256 cannot fit in the bit size 8
+float14.bpl(11,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
+float14.bpl(12,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24
+float14.bpl(15,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 11
+float14.bpl(16,7): error: incorrectly formatted floating point, The given exponent 2048 cannot fit in the bit size 11
+float14.bpl(19,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
+float14.bpl(20,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53
+8 parse errors detected in float14.bpl
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
index e4de8b3b..507c4127 100644
--- a/Test/floats/float3.bpl
+++ b/Test/floats/float3.bpl
@@ -8,20 +8,20 @@ procedure main() returns () {
 	z := x + y;
 	z := x - y;
 	z := x * y;
-	assume(y != 0e-127f24e8);
+	assume(y != 0e0f24e8);
 	z := x / y;
 	
-	z := (0e0f24e8 + 0e0f24e8 + 0e-127f24e8);
-	assert(z == 0e1f24e8);
+	z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8);
+	assert(z == 0e128f24e8);
 	
-	z := 0e1f24e8 - 0e0f24e8;
-	assert(z == 0e0f24e8);
+	z := 0e128f24e8 - 0e127f24e8;
+	assert(z == 0e127f24e8);
 	
-	z := 0e0f24e8 * 0e0f24e8;
-	assert(z == 0e0f24e8);
+	z := 0e127f24e8 * 0e127f24e8;
+	assert(z == 0e127f24e8);
 	
-	z := 0e0f24e8 / 0e0f24e8;
-	assert(z == 0e0f24e8);
+	z := 0e127f24e8 / 0e127f24e8;
+	assert(z == 0e127f24e8);
 	
 	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
index 816d8446..1c2df42e 100644
--- a/Test/floats/float4.bpl
+++ b/Test/floats/float4.bpl
@@ -1,11 +1,19 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 procedure foo() returns (r : float8e24) {
+	var d : float53e11;
+
 	r := 0NaN8e24;
 	r := 0nan8e24;
 	r := 0+oo8e24;
 	r := 0-oo8e24;
-	r := -5e-3f8e24;
+	r := -5e255f8e24;
+	
+	d := 0NaN53e11;
+	d := 0nan53e11;
+	d := 0+oo53e11;
+	d := 0-oo53e11;
+	d := -200e2000f53e11;
 	
 	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl
index c4951681..39fca79e 100644
--- a/Test/floats/float7.bpl
+++ b/Test/floats/float7.bpl
@@ -5,9 +5,9 @@ procedure main() returns () {
 	var y : float53e11;
 	var z : float53e11;
 	var r : float53e11;
-	x := 0e40f53e11;
-	y := x + 0e0f53e11;
-	z := x - 0e0f53e11;
+	x := 0e1063f53e11;
+	y := x + 0e1023f53e11;
+	z := x - 0e1023f53e11;
 	r := y - z;
-	assert r == 0e1f53e11;
+	assert r == 0e1024f53e11;
 }
\ No newline at end of file
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl
index 25c08e4d..bfb3b9e9 100644
--- a/Test/floats/float8.bpl
+++ b/Test/floats/float8.bpl
@@ -5,9 +5,9 @@ procedure main() returns () {
 	var y : float24e8;
 	var z : float24e8;
 	var r : float24e8;
-	x := 0e40f24e8;
-	y := x + 0e0f24e8;
-	z := x - 0e0f24e8;
+	x := 0e167f24e8;
+	y := x + 0e127f24e8;
+	z := x - 0e127f24e8;
 	r := y - z;
-	assert r == 0e1f24e8;
+	assert r == 0e128f24e8;
 }
\ No newline at end of file
-- 
cgit v1.2.3


From f678d42190391708ae09fa68347421da54d9a7b4 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Fri, 22 Jul 2016 16:00:48 -0600
Subject: corrected minor error in test

---
 Test/floats/float13.bpl | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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

diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
index 9b9fa7cb..4aab608a 100644
--- a/Test/floats/float13.bpl
+++ b/Test/floats/float13.bpl
@@ -16,6 +16,10 @@ procedure main() returns () {
 	fc := TO_FLOAT32_INT(5);
 	assert(f == fc);
 	
+	f := -0e126f24e8;
+	fc := TO_FLOAT32_REAL(0.5);
+	assert(f == fc);
+	
 	f := 1048576e128f24e8;
 	fc := TO_FLOAT32_REAL(2.25);
 	assert(f == fc);
@@ -26,5 +30,5 @@ procedure main() returns () {
 	
 	d := 562949953421312e1024f53e11;
 	dc := TO_FLOAT64_REAL(2.25);
-	//assert(d == dc);
+	assert(d == dc);
 }
\ No newline at end of file
-- 
cgit v1.2.3


From 2b64144fb02b68d00188ee81c27afa5fbc026b5b Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Sat, 23 Jul 2016 14:27:23 -0600
Subject: fixed an error where a -0 was not interpreted as a negative number

---
 Source/Basetypes/BigFloat.cs | 4 ++--
 Test/floats/float13.bpl      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index d27a3b00..cb248340 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -144,13 +144,13 @@ namespace Microsoft.Basetypes
       exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1));
       sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1));
       expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1));
+      isNeg = s[0] == '-'; //We do this so that -0 is parsed correctly
       
       if (sigSize <= 0 || expSize <= 0)
         throw new FormatException("Significand and Exponent sizes must be greater than 0");
 
       sigSize = sigSize - 1; //Get rid of sign bit
-      isNeg = sig < 0;
-      sig = BIM.Abs(sig);
+      sig = BIM.Abs(sig); //sig must be positive
       //Uncomment if you want to shift the exponent for the user (i.e. 0e-1f24e8 --> 0e126f24e8)
       //exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One;
 
diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl
index 4aab608a..9c99a30b 100644
--- a/Test/floats/float13.bpl
+++ b/Test/floats/float13.bpl
@@ -17,7 +17,7 @@ procedure main() returns () {
 	assert(f == fc);
 	
 	f := -0e126f24e8;
-	fc := TO_FLOAT32_REAL(0.5);
+	fc := TO_FLOAT32_REAL(-0.5);
 	assert(f == fc);
 	
 	f := 1048576e128f24e8;
-- 
cgit v1.2.3