From 0caf27d014853693836ef06b1706502070b032f6 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 18 Oct 2019 12:12:12 +0200
Subject: Add a check for gradual underflows

---
 kernel/float64.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/float64.ml')

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."
-- 
cgit v1.2.3