diff options
Diffstat (limited to 'test-suite/primitive/float')
| -rw-r--r-- | test-suite/primitive/float/frexp.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/float/ldexp.v | 21 |
2 files changed, 21 insertions, 2 deletions
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v index f13d5cebf6..2a600429b1 100644 --- a/test-suite/primitive/float/frexp.v +++ b/test-suite/primitive/float/frexp.v @@ -1,5 +1,3 @@ -(* TODO add tests for ldexp (particularly with overflow with 31 and 63 bits integers) *) - Require Import ZArith Floats. Definition denorm := Eval compute in ldexp one (-1074)%Z. diff --git a/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v new file mode 100644 index 0000000000..a725deeeca --- /dev/null +++ b/test-suite/primitive/float/ldexp.v @@ -0,0 +1,21 @@ +Require Import ZArith Int63 Floats. + +Check (eq_refl : ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity). +Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity). + +Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity). +Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity). + +Check (eq_refl : ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <: ldexp one (-2102) = 0%float). +Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float). + +Check (eq_refl : ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float). +Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float). + +Check (eq_refl : ldexp one 3 = 8%float). +Check (eq_refl 8%float <: ldexp one 3 = 8%float). +Check (eq_refl 8%float <<: ldexp one 3 = 8%float). |