From c19c2495497d0dfa7aaf871cf833cd5e5f986d33 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 31 May 2016 12:59:38 -0600 Subject: moved all the tests to the testing folder --- Test/floats/test4.bpl | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 Test/floats/test4.bpl (limited to 'Test/floats/test4.bpl') diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl new file mode 100644 index 00000000..a31aa215 --- /dev/null +++ b/Test/floats/test4.bpl @@ -0,0 +1,32 @@ +//Translation from drift_tenth.c +//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 : 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; + //} + 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