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/float4.bpl | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 Test/floats/float4.bpl

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

diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
new file mode 100644
index 00000000..7bb24250
--- /dev/null
+++ b/Test/floats/float4.bpl
@@ -0,0 +1,11 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float32) {
+	r := fp<8, 24>(NaN);
+	r := fp<8, 24>(+oo);
+	r := fp<8, 24>(-oo);
+	r := fp<8, 24>(+zero);
+	r := fp<8, 24>(-zero);
+	
+	return;
+}
\ No newline at end of file
-- 
cgit v1.2.3


From 59052004251c655e06951eb4615938259fdf4844 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Tue, 19 Jul 2016 12:33:21 -0600
Subject: Modified the float tests to match the updated syntax

---
 Test/floats/float0.bpl.expect | 16 ++++-----
 Test/floats/float10.bpl       |  6 ++--
 Test/floats/float11.bpl       | 42 +++++++++++------------
 Test/floats/float12.bpl       | 12 +++----
 Test/floats/float2.bpl        | 28 ++++++++--------
 Test/floats/float2.bpl.expect | 14 ++++----
 Test/floats/float3.bpl        | 24 ++++++-------
 Test/floats/float4.bpl        | 19 +++++------
 Test/floats/float5.bpl        | 45 ++++++++++++-------------
 Test/floats/float5.bpl.expect | 15 ++++-----
 Test/floats/float6.bpl        | 78 ++++++++++++++++---------------------------
 Test/floats/float7.bpl        | 24 ++++++-------
 Test/floats/float8.bpl        | 24 ++++++-------
 Test/floats/float9.bpl        | 32 +++++++++---------
 14 files changed, 177 insertions(+), 202 deletions(-)

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

diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect
index 4c934700..f657a846 100644
--- a/Test/floats/float0.bpl.expect
+++ b/Test/floats/float0.bpl.expect
@@ -1,8 +1,8 @@
-float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float (8 24))
-float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
-float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
-float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float0.bpl(11,23): Error: invalid argument types (float (8 24) and float (8 23)) to binary operator +
-7 type checking errors detected in float0.bpl
+float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float8e24)
+float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float8e24)
+float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float22e8 to float8e24)
+float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
+float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float8e24)
+float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24)
+float0.bpl(11,15): Error: invalid argument types (float24e8 and float23e8) to binary operator +
+7 type checking errors detected in float0.bpl
diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl
index bf07aec6..ec9b4895 100644
--- a/Test/floats/float10.bpl
+++ b/Test/floats/float10.bpl
@@ -1,10 +1,10 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11);
 
 procedure double_range_true() returns () {
-	var x : float64;
+	var x : float53e11;
 	havoc x;
 	if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) {	
 		assert(x==x);
@@ -12,7 +12,7 @@ procedure double_range_true() returns () {
 }
 
 procedure double_range_false() returns () {
-	var x : float64;
+	var x : float53e11;
 	havoc x;
 	assert(x==x);
 }
\ No newline at end of file
diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl
index 424c5a2d..de148424 100644
--- a/Test/floats/float11.bpl
+++ b/Test/floats/float11.bpl
@@ -1,22 +1,22 @@
-// 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 tick : float32;
-	var time : float32;
-	var i: int;
-	
-	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
-	time := TO_FLOAT32_INT(0);
-	
-	i := 0;
-	while (i < 10)
-	{
-		time := time + tick;
-		i := i + 1;
-	}
-	assert time == TO_FLOAT32_INT(1);
+// 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);
+
+procedure main() returns () {
+	var tick : float24e8;
+	var time : float24e8;
+	var i: int;
+	
+	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+	time := TO_FLOAT32_INT(0);
+	
+	i := 0;
+	while (i < 10)
+	{
+		time := time + tick;
+		i := i + 1;
+	}
+	assert time == TO_FLOAT32_INT(1);
 }
\ No newline at end of file
diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl
index 349abb41..914286bb 100644
--- a/Test/floats/float12.bpl
+++ b/Test/floats/float12.bpl
@@ -1,14 +1,14 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-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);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) 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 x : float64;
-	var y : float32;
+	var x : float53e11;
+	var y : float24e8;
 	
 	x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1);
 	y := TO_FLOAT32_FLOAT64(x);
diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl
index 1a4d02cd..ed9e60f0 100644
--- a/Test/floats/float2.bpl
+++ b/Test/floats/float2.bpl
@@ -1,15 +1,15 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo(x : float16) returns(r : float32) {
-	var y : float64;
-	var z : float128;
-	
-	r := x; // Error
-	r := y; // Error
-	r := z; // Error
-	y := x; // Error
-	y := z; // Error
-	z := x; // Error
-
-	return;
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float11e5) returns(r : float24e8) {
+	var y : float53e11;
+	var z : float113e15;
+	
+	r := x; // Error
+	r := y; // Error
+	r := z; // Error
+	y := x; // Error
+	y := z; // Error
+	z := x; // Error
+
+	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect
index 62348741..3132c514 100644
--- a/Test/floats/float2.bpl.expect
+++ b/Test/floats/float2.bpl.expect
@@ -1,7 +1,7 @@
-float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (8 24))
-float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (11 53) to float (8 24))
-float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (8 24))
-float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (11 53))
-float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (11 53))
-float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (15 113))
-6 type checking errors detected in float2.bpl
+float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float11e5 to float24e8)
+float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float53e11 to float24e8)
+float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float113e15 to float24e8)
+float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float11e5 to float53e11)
+float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float113e15 to float53e11)
+float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float11e5 to float113e15)
+6 type checking errors detected in float2.bpl
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
index 240c02f3..31de7ca8 100644
--- a/Test/floats/float3.bpl
+++ b/Test/floats/float3.bpl
@@ -1,27 +1,27 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 procedure main() returns () {
-	var x : float32;
-	var y : float32;
-	var z : float32;
+	var x : float24e8;
+	var y : float24e8;
+	var z : float24e8;
 	
 	z := x + y;
 	z := x - y;
 	z := x * y;
-	assume(y != fp<8, 24>(0bv32));
+	assume(y != 0e-128f24e8);
 	z := x / y;
 	
-	z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);
-	assert(z == fp<8, 24>(2bv32));
+	z := (0e0f24e8 + 0e0f24e8 + 0e-128f24e8);
+	assert(z == 0e1f24e8);
 	
-	z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32);
-	assert(z == fp<8, 24>(1bv32));
+	z := 0e1f24e8 - 0e0f24e8;
+	assert(z == 0e0f24e8);
 	
-	z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);
-	assert(z == fp(false, 127bv8, 0bv23));
+	z := 0e0f24e8 * 0e0f24e8;
+	assert(z == 0e0f24e8);
 	
-	z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);
-	assert(z == fp(false, 127bv8, 0bv23));
+	z := 0e0f24e8 / 0e0f24e8;
+	assert(z == 0e0f24e8);
 	
 	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
index 7bb24250..a1608572 100644
--- a/Test/floats/float4.bpl
+++ b/Test/floats/float4.bpl
@@ -1,11 +1,10 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo() returns (r : float32) {
-	r := fp<8, 24>(NaN);
-	r := fp<8, 24>(+oo);
-	r := fp<8, 24>(-oo);
-	r := fp<8, 24>(+zero);
-	r := fp<8, 24>(-zero);
-	
-	return;
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float32) {
+	r := 0NaN8e24;
+	r := 0nan8e24;
+	r := 0+oo8e24;
+	r := 0-oo8e24;
+	
+	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl
index fd630394..12b19cf5 100644
--- a/Test/floats/float5.bpl
+++ b/Test/floats/float5.bpl
@@ -1,24 +1,23 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float<8, 23>);
-function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float<8, 23>);
-function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float<8, 23>);
-function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float<8, 23>);
-function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float<8, 24>) returns (float<8, 23>);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float<8, 23>) returns (float<8, 24>);
-
-procedure foo(x : float<8, 24>) returns (r : float<8, 24>) {
-	r := TO_FLOAT823_INT(5); // Error
-	r := TO_FLOAT823_REAL(5.0); // Error
-	r := TO_FLOAT823_BV31(0bv31); // Error
-	r := TO_FLOAT823_BV32(0bv32); // Error
-	r := TO_FLOAT823_FLOAT824(fp<8, 24>(1bv32)); // Error
-	r := TO_FLOAT824_FLOAT823(fp<8, 24>(1bv32)); // Error
-	r := TO_FLOAT824_FLOAT823(fp<8, 23>(1bv31));
-	
-	r := TO_FLOAT823_FLOAT824(x); // Error
-	r := TO_FLOAT824_FLOAT823(x); // Error
-	
-	return;
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float23e8);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float24e8) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float23e8) returns (float24e8);
+
+procedure foo(x : float24e8) returns (r : float24e8) {
+	r := TO_FLOAT823_INT(5); // Error
+	r := TO_FLOAT823_REAL(5.0); // Error
+	r := TO_FLOAT823_BV31(0bv31); // Error
+	r := TO_FLOAT823_BV32(0bv32); // Error
+	r := TO_FLOAT823_FLOAT824(0e0f24e8); // Error
+	r := TO_FLOAT824_FLOAT823(0e0f23e8); // Error
+	
+	r := TO_FLOAT823_FLOAT824(x); // Error
+	r := TO_FLOAT824_FLOAT823(x); // Error
+	
+	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect
index 6c0b86af..74649769 100644
--- a/Test/floats/float5.bpl.expect
+++ b/Test/floats/float5.bpl.expect
@@ -1,9 +1,6 @@
-float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(16,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(17,42): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
-float5.bpl(20,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
-float5.bpl(21,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
-8 type checking errors detected in float5.bpl
+float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8)
+float5.bpl(20,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float24e8 (expected: float23e8)
+5 type checking errors detected in float5.bpl
diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl
index fe0eab0e..fecf0385 100644
--- a/Test/floats/float6.bpl
+++ b/Test/floats/float6.bpl
@@ -1,50 +1,30 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_INT(int) returns (float<8, 24>);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_REAL(real) returns (float<8, 24>);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_BV32(bv32) returns (float<8, 24>);
-function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT1153_BV64(bv64) returns (float<11, 53>);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT32(float32) returns (float<8, 24>);  //Should just be an identity function
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT824(float<8, 24>) returns (float32); //Should just be an identity function
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);
-function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);
-
-procedure main() returns () {
-	var i : int;
-	var r : real;
-	var f824 : float<8, 24>;
-	var f32 : float32;
-	var f1153 : float<11, 53>;
-	var f64 : float64;
-	
-	f824 := TO_FLOAT824_INT(5);
-	f32 := TO_FLOAT824_INT(5);
-	f824 := TO_FLOAT824_REAL(5.0);
-	f32 := TO_FLOAT824_REAL(5.0);
-	
-	f824 := TO_FLOAT824_BV32(0bv32);
-	f32 := TO_FLOAT824_BV32(0bv32);
-	f1153 := TO_FLOAT1153_BV64(0bv64);
-	f64 := TO_FLOAT1153_BV64(0bv64);
-	
-	f824 := TO_FLOAT824_FLOAT32(fp<8, 24>(0bv32));
-	f32 := TO_FLOAT32_FLOAT824(fp<8, 24>(0bv32));
-	f824 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
-	f32 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
-	f1153 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
-	f64 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
-	
-	f824 := TO_FLOAT824_INT(5);
-	f32 := TO_FLOAT32_FLOAT824(f824);
-	assert(f32 == f824);
-	
-	f32 := TO_FLOAT824_INT(5);
-	f824 := TO_FLOAT824_FLOAT32(f32);
-	assert(f32 == f824);
-	
-	f32 := TO_FLOAT32_FLOAT64(f64);
-	f64 := TO_FLOAT64_FLOAT32(f32);
-	
-	return;
+// 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 8 24) RNE"} TO_FLOAT32_BV32(bv32) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_BV64(bv64) returns (float53e11);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11);
+
+procedure main() returns () {
+	var i : int;
+	var r : real;
+	var f32 : float24e8;
+	var f64 : float53e11;
+	
+	f32 := TO_FLOAT32_INT(5);
+	f32 := TO_FLOAT32_REAL(5.0);
+	
+	f32 := TO_FLOAT32_BV32(0bv32);
+	f64 := TO_FLOAT64_BV64(0bv64);
+	
+	f32 := TO_FLOAT32_FLOAT64(0e0f53e11);
+	f64 := TO_FLOAT64_FLOAT32(0e0f24e8);
+	
+	f32 := TO_FLOAT32_FLOAT64(f64);
+	f64 := TO_FLOAT64_FLOAT32(f32);
+	
+	return;
 }
\ No newline at end of file
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl
index f330b2ea..c4951681 100644
--- a/Test/floats/float7.bpl
+++ b/Test/floats/float7.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main() returns () {
-	var x : float<11, 53>;
-	var y : float<11, 53>;
-	var z : float<11, 53>;
-	var r : float<11, 53>;
-	x := fp<11, 53> (10000000bv64);
-	y := x + fp<11, 53>(1bv64);
-	z := x - fp<11, 53>(1bv64);
-	r := y - z;
-	assert r == fp<11, 53> (2bv64);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+	var x : float53e11;
+	var y : float53e11;
+	var z : float53e11;
+	var r : float53e11;
+	x := 0e40f53e11;
+	y := x + 0e0f53e11;
+	z := x - 0e0f53e11;
+	r := y - z;
+	assert r == 0e1f53e11;
 }
\ No newline at end of file
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl
index 78c11a2b..25c08e4d 100644
--- a/Test/floats/float8.bpl
+++ b/Test/floats/float8.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main() returns () {
-	var x : float32;
-	var y : float32;
-	var z : float32;
-	var r : float32;
-	x := fp<8, 24>(3221225472bv32);
-	y := x + fp<8, 24>(1bv32);
-	z := x - fp<8, 24>(1bv32);
-	r := y - z;
-	assert r == fp<8, 24>(2bv32);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+	var x : float24e8;
+	var y : float24e8;
+	var z : float24e8;
+	var r : float24e8;
+	x := 0e40f24e8;
+	y := x + 0e0f24e8;
+	z := x - 0e0f24e8;
+	r := y - z;
+	assert r == 0e1f24e8;
 }
\ No newline at end of file
diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl
index cb4f3afd..b1e46ae4 100644
--- a/Test/floats/float9.bpl
+++ b/Test/floats/float9.bpl
@@ -1,17 +1,17 @@
-// 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;
-	var r : float32;
-	x := TO_FLOAT32_REAL(1e7);
-	y := x + TO_FLOAT32_INT(1);
-	z := x - TO_FLOAT32_INT(1);
-	r := y - z;
-	assert r == TO_FLOAT32_INT(2);
+// 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);
+
+procedure main() returns () {
+	var x : float24e8;
+	var y : float24e8;
+	var z : float24e8;
+	var r : float24e8;
+	x := TO_FLOAT32_REAL(1e7);
+	y := x + TO_FLOAT32_INT(1);
+	z := x - TO_FLOAT32_INT(1);
+	r := y - z;
+	assert r == TO_FLOAT32_INT(2);
 }
\ No newline at end of file
-- 
cgit v1.2.3


From 86c78db45fad37209663bf87547a50a880760051 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Tue, 19 Jul 2016 16:39:54 -0600
Subject: fixed an issue with parsing floating points

---
 Source/Core/BoogiePL.atg |  12 +-
 Source/Core/Parser.cs    |   5 +-
 Source/Core/Scanner.cs   | 363 ++++++++++++++++++++++++++++++-----------------
 Test/floats/float3.bpl   |   4 +-
 Test/floats/float4.bpl   |   3 +-
 5 files changed, 249 insertions(+), 138 deletions(-)

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

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 31823110..f74f8bff 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -145,7 +145,11 @@ TOKENS
 
   decimal = digit {digit} 'e' [ '-' ] digit {digit} .
   dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
-		float = digit {digit} 'e' digit {digit} 'f' digit {digit} 'e' digit {digit} .
+		float = [ '-' ] digit {digit} 'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit} 
+										| '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit}
+										| '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit}
+										| '0' '+' 'o' 'o' digit {digit} 'e' digit {digit}
+										| '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} .
 
 COMMENTS FROM "/*" TO "*/" NESTED
 COMMENTS FROM "//" TO lf
@@ -1292,7 +1296,7 @@ AtomExpression<out Expr/*!*/ e>
     Expression<out e>
     ")"                     (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .)
 
-  | "(" ( Expression<out e>                 (. if (e is BvBounds)
+		| "(" ( Expression<out e>                 (. if (e is BvBounds)
                                                  this.SemErr("parentheses around bitvector bounds " +
                                                         "are not allowed"); .)
         | Forall                            (. x = t; .)
@@ -1518,8 +1522,8 @@ Float<out BigFloat n>
   )
   (. try {
        n = BigFloat.FromString(s);
-     } catch (FormatException) {
-       this.SemErr("incorrectly formatted number");
+     } catch (FormatException e) {
+       this.SemErr("incorrectly formatted floating point, " + e.Message);
        n = BigFloat.ZERO;
      }
   .)
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index a5e2921e..c91de177 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -133,7 +133,8 @@ private class BvBounds : Expr {
     Contract.Assert(false);throw new cce.UnreachableException();
   }
   public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
-  public override int ComputeHashCode() {
+  public override int ComputeHashCode()
+  {
     return base.GetHashCode();
   }
 }
@@ -1866,7 +1867,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		try {
 		 n = BigFloat.FromString(s);
 		} catch (FormatException e) {
-		 this.SemErr("incorrectly formatted floating point: " + e.Message);
+		 this.SemErr("incorrectly formatted floating point, " + e.Message);
 		 n = BigFloat.ZERO;
 		}
 		
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 1185963f..46a3c419 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -267,41 +267,42 @@ public class Scanner {
 		for (int i = 65; i <= 90; ++i) start[i] = 2;
 		for (int i = 94; i <= 122; ++i) start[i] = 2;
 		for (int i = 126; i <= 126; ++i) start[i] = 2;
-		for (int i = 48; i <= 57; ++i) start[i] = 19;
+		for (int i = 49; i <= 57; ++i) start[i] = 45;
 		for (int i = 34; i <= 34; ++i) start[i] = 6;
 		start[92] = 1; 
-		start[59] = 24; 
-		start[40] = 25; 
-		start[41] = 26; 
-		start[58] = 60; 
-		start[44] = 27; 
-		start[91] = 28; 
-		start[93] = 29; 
-		start[60] = 61; 
-		start[62] = 62; 
-		start[123] = 30; 
-		start[125] = 63; 
-		start[61] = 64; 
-		start[42] = 65; 
-		start[124] = 66; 
-		start[8660] = 33; 
-		start[8658] = 35; 
-		start[8656] = 36; 
-		start[38] = 37; 
-		start[8743] = 39; 
-		start[8744] = 41; 
-		start[33] = 67; 
-		start[8800] = 45; 
-		start[8804] = 46; 
-		start[8805] = 47; 
-		start[43] = 68; 
-		start[45] = 49; 
-		start[47] = 50; 
-		start[172] = 52; 
-		start[8704] = 55; 
-		start[8707] = 56; 
-		start[955] = 57; 
-		start[8226] = 59; 
+		start[45] = 87; 
+		start[48] = 46; 
+		start[59] = 52; 
+		start[40] = 53; 
+		start[41] = 54; 
+		start[58] = 88; 
+		start[44] = 55; 
+		start[91] = 56; 
+		start[93] = 57; 
+		start[60] = 89; 
+		start[62] = 90; 
+		start[123] = 58; 
+		start[125] = 91; 
+		start[61] = 92; 
+		start[42] = 93; 
+		start[124] = 94; 
+		start[8660] = 61; 
+		start[8658] = 63; 
+		start[8656] = 64; 
+		start[38] = 65; 
+		start[8743] = 67; 
+		start[8744] = 69; 
+		start[33] = 95; 
+		start[8800] = 73; 
+		start[8804] = 74; 
+		start[8805] = 75; 
+		start[43] = 96; 
+		start[47] = 77; 
+		start[172] = 79; 
+		start[8704] = 82; 
+		start[8707] = 83; 
+		start[955] = 84; 
+		start[8226] = 86; 
 		start[Buffer.EOF] = -1;
 
 	}
@@ -597,7 +598,7 @@ public class Scanner {
 			case 6:
 				if (ch == '"') {AddCh(); goto case 7;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 20;}
+				else if (ch == 92) {AddCh(); goto case 47;}
 				else {goto case 0;}
 			case 7:
 				{t.kind = 4; break;}
@@ -605,192 +606,296 @@ public class Scanner {
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
 				else {goto case 0;}
 			case 9:
-				recEnd = pos; recKind = 5;
+				recEnd = pos; recKind = 6;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
-				else {t.kind = 5; break;}
+				else if (ch == 'e') {AddCh(); goto case 10;}
+				else {t.kind = 6; break;}
 			case 10:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+				else if (ch == '-') {AddCh(); goto case 11;}
 				else {goto case 0;}
 			case 11:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+				else {goto case 0;}
+			case 12:
 				recEnd = pos; recKind = 6;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;}
-				else if (ch == 'e') {AddCh(); goto case 12;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
 				else {t.kind = 6; break;}
-			case 12:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
-				else if (ch == '-') {AddCh(); goto case 13;}
-				else {goto case 0;}
 			case 13:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+				else if (ch == 'e') {AddCh(); goto case 14;}
 				else {goto case 0;}
 			case 14:
-				recEnd = pos; recKind = 6;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;}
-				else {t.kind = 6; break;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+				else if (ch == '-') {AddCh(); goto case 15;}
+				else {goto case 0;}
 			case 15:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
 				else {goto case 0;}
 			case 16:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
-				else if (ch == 'e') {AddCh(); goto case 17;}
+				else if (ch == 'f') {AddCh(); goto case 17;}
 				else {goto case 0;}
 			case 17:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
 				else {goto case 0;}
 			case 18:
-				recEnd = pos; recKind = 7;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
-				else {t.kind = 7; break;}
+				else if (ch == 'e') {AddCh(); goto case 19;}
+				else {goto case 0;}
 			case 19:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+				else {goto case 0;}
+			case 20:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+				else {t.kind = 7; break;}
+			case 21:
+				if (ch == 'a') {AddCh(); goto case 22;}
+				else {goto case 0;}
+			case 22:
+				if (ch == 'N') {AddCh(); goto case 23;}
+				else {goto case 0;}
+			case 23:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+				else {goto case 0;}
+			case 24:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+				else if (ch == 'e') {AddCh(); goto case 25;}
+				else {goto case 0;}
+			case 25:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+				else {goto case 0;}
+			case 26:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+				else {t.kind = 7; break;}
+			case 27:
+				if (ch == 'a') {AddCh(); goto case 28;}
+				else {goto case 0;}
+			case 28:
+				if (ch == 'n') {AddCh(); goto case 29;}
+				else {goto case 0;}
+			case 29:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+				else {goto case 0;}
+			case 30:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+				else if (ch == 'e') {AddCh(); goto case 31;}
+				else {goto case 0;}
+			case 31:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
+				else {goto case 0;}
+			case 32:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
+				else {t.kind = 7; break;}
+			case 33:
+				if (ch == 'o') {AddCh(); goto case 34;}
+				else {goto case 0;}
+			case 34:
+				if (ch == 'o') {AddCh(); goto case 35;}
+				else {goto case 0;}
+			case 35:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+				else {goto case 0;}
+			case 36:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+				else if (ch == 'e') {AddCh(); goto case 37;}
+				else {goto case 0;}
+			case 37:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+				else {goto case 0;}
+			case 38:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+				else {t.kind = 7; break;}
+			case 39:
+				if (ch == 'o') {AddCh(); goto case 40;}
+				else {goto case 0;}
+			case 40:
+				if (ch == 'o') {AddCh(); goto case 41;}
+				else {goto case 0;}
+			case 41:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+				else {goto case 0;}
+			case 42:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+				else if (ch == 'e') {AddCh(); goto case 43;}
+				else {goto case 0;}
+			case 43:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+				else {goto case 0;}
+			case 44:
+				recEnd = pos; recKind = 7;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+				else {t.kind = 7; break;}
+			case 45:
 				recEnd = pos; recKind = 3;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
 				else if (ch == 'b') {AddCh(); goto case 3;}
-				else if (ch == 'e') {AddCh(); goto case 21;}
-				else if (ch == '.') {AddCh(); goto case 10;}
+				else if (ch == 'e') {AddCh(); goto case 48;}
+				else if (ch == '.') {AddCh(); goto case 8;}
 				else {t.kind = 3; break;}
-			case 20:
-				if (ch == '"') {AddCh(); goto case 22;}
+			case 46:
+				recEnd = pos; recKind = 3;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
+				else if (ch == 'b') {AddCh(); goto case 3;}
+				else if (ch == 'e') {AddCh(); goto case 48;}
+				else if (ch == '.') {AddCh(); goto case 8;}
+				else if (ch == 'N') {AddCh(); goto case 21;}
+				else if (ch == 'n') {AddCh(); goto case 27;}
+				else if (ch == '+') {AddCh(); goto case 33;}
+				else if (ch == '-') {AddCh(); goto case 39;}
+				else {t.kind = 3; break;}
+			case 47:
+				if (ch == '"') {AddCh(); goto case 49;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 20;}
+				else if (ch == 92) {AddCh(); goto case 47;}
 				else {goto case 0;}
-			case 21:
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
-				else if (ch == '-') {AddCh(); goto case 8;}
+			case 48:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+				else if (ch == '-') {AddCh(); goto case 51;}
 				else {goto case 0;}
-			case 22:
+			case 49:
 				recEnd = pos; recKind = 4;
 				if (ch == '"') {AddCh(); goto case 7;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
-				else if (ch == 92) {AddCh(); goto case 20;}
+				else if (ch == 92) {AddCh(); goto case 47;}
 				else {t.kind = 4; break;}
-			case 23:
+			case 50:
 				recEnd = pos; recKind = 5;
-				if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;}
-				else if (ch == 'f') {AddCh(); goto case 15;}
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+				else if (ch == 'f') {AddCh(); goto case 17;}
 				else {t.kind = 5; break;}
-			case 24:
+			case 51:
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+				else {goto case 0;}
+			case 52:
 				{t.kind = 9; break;}
-			case 25:
+			case 53:
 				{t.kind = 10; break;}
-			case 26:
+			case 54:
 				{t.kind = 11; break;}
-			case 27:
+			case 55:
 				{t.kind = 13; break;}
-			case 28:
+			case 56:
 				{t.kind = 18; break;}
-			case 29:
+			case 57:
 				{t.kind = 19; break;}
-			case 30:
+			case 58:
 				{t.kind = 28; break;}
-			case 31:
+			case 59:
 				{t.kind = 51; break;}
-			case 32:
+			case 60:
 				{t.kind = 56; break;}
-			case 33:
+			case 61:
 				{t.kind = 57; break;}
-			case 34:
+			case 62:
 				{t.kind = 58; break;}
-			case 35:
+			case 63:
 				{t.kind = 59; break;}
-			case 36:
+			case 64:
 				{t.kind = 61; break;}
-			case 37:
-				if (ch == '&') {AddCh(); goto case 38;}
+			case 65:
+				if (ch == '&') {AddCh(); goto case 66;}
 				else {goto case 0;}
-			case 38:
+			case 66:
 				{t.kind = 62; break;}
-			case 39:
+			case 67:
 				{t.kind = 63; break;}
-			case 40:
+			case 68:
 				{t.kind = 64; break;}
-			case 41:
+			case 69:
 				{t.kind = 65; break;}
-			case 42:
+			case 70:
 				{t.kind = 68; break;}
-			case 43:
+			case 71:
 				{t.kind = 69; break;}
-			case 44:
+			case 72:
 				{t.kind = 70; break;}
-			case 45:
+			case 73:
 				{t.kind = 71; break;}
-			case 46:
+			case 74:
 				{t.kind = 72; break;}
-			case 47:
+			case 75:
 				{t.kind = 73; break;}
-			case 48:
+			case 76:
 				{t.kind = 74; break;}
-			case 49:
-				{t.kind = 76; break;}
-			case 50:
+			case 77:
 				{t.kind = 79; break;}
-			case 51:
+			case 78:
 				{t.kind = 80; break;}
-			case 52:
+			case 79:
 				{t.kind = 82; break;}
-			case 53:
+			case 80:
 				{t.kind = 86; break;}
-			case 54:
+			case 81:
 				{t.kind = 87; break;}
-			case 55:
+			case 82:
 				{t.kind = 90; break;}
-			case 56:
+			case 83:
 				{t.kind = 92; break;}
-			case 57:
+			case 84:
 				{t.kind = 94; break;}
-			case 58:
+			case 85:
 				{t.kind = 95; break;}
-			case 59:
+			case 86:
 				{t.kind = 96; break;}
-			case 60:
+			case 87:
+				recEnd = pos; recKind = 76;
+				if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+				else {t.kind = 76; break;}
+			case 88:
 				recEnd = pos; recKind = 12;
-				if (ch == '=') {AddCh(); goto case 31;}
-				else if (ch == ':') {AddCh(); goto case 58;}
+				if (ch == '=') {AddCh(); goto case 59;}
+				else if (ch == ':') {AddCh(); goto case 85;}
 				else {t.kind = 12; break;}
-			case 61:
+			case 89:
 				recEnd = pos; recKind = 20;
-				if (ch == '=') {AddCh(); goto case 69;}
-				else if (ch == ':') {AddCh(); goto case 44;}
+				if (ch == '=') {AddCh(); goto case 97;}
+				else if (ch == ':') {AddCh(); goto case 72;}
 				else {t.kind = 20; break;}
-			case 62:
+			case 90:
 				recEnd = pos; recKind = 21;
-				if (ch == '=') {AddCh(); goto case 42;}
+				if (ch == '=') {AddCh(); goto case 70;}
 				else {t.kind = 21; break;}
-			case 63:
+			case 91:
 				recEnd = pos; recKind = 29;
-				if (ch == '|') {AddCh(); goto case 54;}
+				if (ch == '|') {AddCh(); goto case 81;}
 				else {t.kind = 29; break;}
-			case 64:
+			case 92:
 				recEnd = pos; recKind = 32;
-				if (ch == '=') {AddCh(); goto case 70;}
+				if (ch == '=') {AddCh(); goto case 98;}
 				else {t.kind = 32; break;}
-			case 65:
+			case 93:
 				recEnd = pos; recKind = 45;
-				if (ch == '*') {AddCh(); goto case 51;}
+				if (ch == '*') {AddCh(); goto case 78;}
 				else {t.kind = 45; break;}
-			case 66:
+			case 94:
 				recEnd = pos; recKind = 55;
-				if (ch == '|') {AddCh(); goto case 40;}
-				else if (ch == '{') {AddCh(); goto case 53;}
+				if (ch == '|') {AddCh(); goto case 68;}
+				else if (ch == '{') {AddCh(); goto case 80;}
 				else {t.kind = 55; break;}
-			case 67:
+			case 95:
 				recEnd = pos; recKind = 81;
-				if (ch == '=') {AddCh(); goto case 43;}
+				if (ch == '=') {AddCh(); goto case 71;}
 				else {t.kind = 81; break;}
-			case 68:
+			case 96:
 				recEnd = pos; recKind = 75;
-				if (ch == '+') {AddCh(); goto case 48;}
+				if (ch == '+') {AddCh(); goto case 76;}
 				else {t.kind = 75; break;}
-			case 69:
+			case 97:
 				recEnd = pos; recKind = 67;
-				if (ch == '=') {AddCh(); goto case 71;}
+				if (ch == '=') {AddCh(); goto case 99;}
 				else {t.kind = 67; break;}
-			case 70:
+			case 98:
 				recEnd = pos; recKind = 66;
-				if (ch == '>') {AddCh(); goto case 34;}
+				if (ch == '>') {AddCh(); goto case 62;}
 				else {t.kind = 66; break;}
-			case 71:
+			case 99:
 				recEnd = pos; recKind = 60;
-				if (ch == '>') {AddCh(); goto case 32;}
+				if (ch == '>') {AddCh(); goto case 60;}
 				else {t.kind = 60; break;}
 
 		}
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
index 31de7ca8..e4de8b3b 100644
--- a/Test/floats/float3.bpl
+++ b/Test/floats/float3.bpl
@@ -8,10 +8,10 @@ procedure main() returns () {
 	z := x + y;
 	z := x - y;
 	z := x * y;
-	assume(y != 0e-128f24e8);
+	assume(y != 0e-127f24e8);
 	z := x / y;
 	
-	z := (0e0f24e8 + 0e0f24e8 + 0e-128f24e8);
+	z := (0e0f24e8 + 0e0f24e8 + 0e-127f24e8);
 	assert(z == 0e1f24e8);
 	
 	z := 0e1f24e8 - 0e0f24e8;
diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
index a1608572..816d8446 100644
--- a/Test/floats/float4.bpl
+++ b/Test/floats/float4.bpl
@@ -1,10 +1,11 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-procedure foo() returns (r : float32) {
+procedure foo() returns (r : float8e24) {
 	r := 0NaN8e24;
 	r := 0nan8e24;
 	r := 0+oo8e24;
 	r := 0-oo8e24;
+	r := -5e-3f8e24;
 	
 	return;
 }
\ 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/float4.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