diff options
| author | Pierre Roux | 2019-10-18 12:12:12 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:47 +0100 |
| commit | 0caf27d014853693836ef06b1706502070b032f6 (patch) | |
| tree | ae7ffc8f25aa8259632345f1b4cf6119be341de3 | |
| parent | 3b1edf7cf689a54d03226072dd3b359026588e26 (diff) | |
Add a check for gradual underflows
| -rw-r--r-- | configure.ml | 7 | ||||
| -rw-r--r-- | kernel/float64.ml | 7 |
2 files changed, 7 insertions, 7 deletions
diff --git a/configure.ml b/configure.ml index 5f326425fc..af07ec4bb0 100644 --- a/configure.ml +++ b/configure.ml @@ -944,9 +944,10 @@ let () = let add = (+.) in let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in - if (add b s <= b || add b 1. <> b) && not sse2_math then - die "Detected double-rounding due to the use of intermediate \ - 80-bit floating-point representation, and SSE2_MATH is not available." + if (add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0.) + && not sse2_math then + die "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." (** * OCaml runtime flags *) diff --git a/kernel/float64.ml b/kernel/float64.ml index c08069f3e3..3e36373b77 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -154,7 +154,6 @@ let is_float64 t = let () = let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in - if add b s <= b || add b 1. <> b then - failwith "Detected double-rounding due to the use of intermediate \ - 80-bit floating-point representation. Use of Float is \ - thus unsafe." + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." |