diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-05-31 12:08:07 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-05-31 12:08:07 -0600 |
commit | 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 (patch) | |
tree | 6d55790d0180d5e8cf1a79ea03ad6ce3b2019f17 /float_test5.bpl | |
parent | 51b7e8146f413b83a412572fcc9e3a1a8b302b79 (diff) |
Initial round of testing works with new syntax. Fixed an error where floating points could not be given as a function argument
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) |