diff options
Diffstat (limited to 'Test/floats/test4.bpl')
-rw-r--r-- | Test/floats/test4.bpl | 32 |
1 files changed, 32 insertions, 0 deletions
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 |