diff options
Diffstat (limited to 'test-suite/primitive/float')
| -rw-r--r-- | test-suite/primitive/float/frexp.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v index 2a600429b1..f13d5cebf6 100644 --- a/test-suite/primitive/float/frexp.v +++ b/test-suite/primitive/float/frexp.v @@ -1,3 +1,5 @@ +(* 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. |