diff options
Diffstat (limited to 'Test/floats/float12.bpl')
| -rw-r--r-- | Test/floats/float12.bpl | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl index 349abb41..914286bb 100644 --- a/Test/floats/float12.bpl +++ b/Test/floats/float12.bpl @@ -1,14 +1,14 @@ // RUN: %boogie -proverWarnings:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -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); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); procedure main() returns () { - var x : float64; - var y : float32; + var x : float53e11; + var y : float24e8; x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); y := TO_FLOAT32_FLOAT64(x); |