diff options
Diffstat (limited to 'float_test5.bpl')
| -rw-r--r-- | float_test5.bpl | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/float_test5.bpl b/float_test5.bpl index ce5d2bc7..7536f8fd 100644 --- a/float_test5.bpl +++ b/float_test5.bpl @@ -1,15 +1,18 @@ //Translation from filter1.c //Should Verify +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + procedure main() returns () { - var E0 : float(11 53); - var E1 : float(11 53); - var S : float(11 53); + var E0 : float64; + var E1 : float64; + var S : float64); var i : int; var rand : int; - E1 := fp(0 11 53); - S := fp(0 11 53); + E1 := TO_FLOAT64_INT(0); + S := TO_FLOAT64_INT(0); i := 0; while (i <= 1000000) |