diff options
Diffstat (limited to 'float_test4.bpl')
| -rw-r--r-- | float_test4.bpl | 38 |
1 files changed, 25 insertions, 13 deletions
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 |