summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/floats/float0.bpl.expect16
-rw-r--r--Test/floats/float10.bpl6
-rw-r--r--Test/floats/float11.bpl42
-rw-r--r--Test/floats/float12.bpl12
-rw-r--r--Test/floats/float2.bpl28
-rw-r--r--Test/floats/float2.bpl.expect14
-rw-r--r--Test/floats/float3.bpl24
-rw-r--r--Test/floats/float4.bpl19
-rw-r--r--Test/floats/float5.bpl45
-rw-r--r--Test/floats/float5.bpl.expect15
-rw-r--r--Test/floats/float6.bpl78
-rw-r--r--Test/floats/float7.bpl24
-rw-r--r--Test/floats/float8.bpl24
-rw-r--r--Test/floats/float9.bpl32
14 files changed, 177 insertions, 202 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 11:05:16 +0000