diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:11:23 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 21:11:23 -0600 |
commit | 754f7d3ef36e11740a40a2d687f3b15195f63d9a (patch) | |
tree | 25b2ca0d03416aa6873680424fc481aeed004d67 /Test/floats/float18.bpl | |
parent | 5cff8cd77c629ec8e48a2498b1e704173306586a (diff) |
Polished up the floats test folder. Preparing to rebase
Diffstat (limited to 'Test/floats/float18.bpl')
-rw-r--r-- | Test/floats/float18.bpl | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/Test/floats/float18.bpl b/Test/floats/float18.bpl deleted file mode 100644 index 7e78e206..00000000 --- a/Test/floats/float18.bpl +++ /dev/null @@ -1,16 +0,0 @@ -//Translation from float_double.c -//Should Verify - -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); -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 x : float64; - var y : float32; - - x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); - y := TO_FLOAT32_FLOAT64(x); - assert x != TO_FLOAT64_FLOAT32(y); -}
\ No newline at end of file |