From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 4 Apr 2019 00:14:47 +0200
Subject: Make primitive float work on x86_32

Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.

Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.

Add a runtime test for double roundings.
---
 test-suite/primitive/float/frexp.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite/primitive/float')

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