diff options
Diffstat (limited to 'Test/floats/test4.bpl')
-rw-r--r-- | Test/floats/test4.bpl | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl deleted file mode 100644 index a31aa215..00000000 --- a/Test/floats/test4.bpl +++ /dev/null @@ -1,32 +0,0 @@ -//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 |