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/float11.bpl | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Test/floats/float11.bpl') 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 -- cgit v1.2.3