From 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 31 May 2016 12:08:07 -0600 Subject: Initial round of testing works with new syntax. Fixed an error where floating points could not be given as a function argument --- float_test4.bpl | 38 +++++++++++++++++++++++++------------- 1 file changed, 25 insertions(+), 13 deletions(-) (limited to 'float_test4.bpl') diff --git a/float_test4.bpl b/float_test4.bpl index a7aa8c4b..a31aa215 100644 --- a/float_test4.bpl +++ b/float_test4.bpl @@ -1,20 +1,32 @@ //Translation from drift_tenth.c -//Should Verify -//FAILS; note that it succeeds when tick == fp(.1) +//Should Fail + +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 : float; - var time : float; + var tick : float32; + var time : float32; var i: int; - tick := fp(1)/fp(10); - time := fp(0); + 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 == fp(1)); + //i := 0; + //while (i < 10) + //{ + // time := time + tick; + // i := i + 1; + //} + time := time + tick;//1 + time := time + tick;//2 + time := time + tick;//3 + time := time + tick;//4 + time := time + tick;//5 + time := time + tick;//6 + time := time + tick;//7 + time := time + tick;//8 + time := time + tick;//9 + time := time + tick;//10 + assert time == TO_FLOAT32_INT(1); } \ No newline at end of file -- cgit v1.2.3