From 59052004251c655e06951eb4615938259fdf4844 Mon Sep 17 00:00:00 2001 From: Checkmate50 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(-) 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