diff options
| author | Pierre Roux | 2019-04-19 15:29:53 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:11 +0100 |
| commit | f8fdc27f922694edf74a7b608de1596e0a1ac0e3 (patch) | |
| tree | 8c101e668ea50a1c39420e432d0382edc40b98b2 | |
| parent | a2ba4016a64f84193261db9a52196adc39cb5767 (diff) | |
Make primitive float work on Windows
| -rw-r--r-- | kernel/byterun/coq_interp.c | 6 | ||||
| -rw-r--r-- | test-suite/output/FloatSyntax.out | 8 | ||||
| -rw-r--r-- | test-suite/output/FloatSyntax.v | 11 |
3 files changed, 17 insertions, 8 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e67325eb9a..6e6adb1293 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1652,6 +1652,12 @@ value coq_interprete double f; print_instr("CHECKFRSHIFTEXP"); CheckFloat1(); + /* frexp(infinity) incorrectly returns nan on mingw */ +#if defined(__MINGW32__) || defined(__MINGW64__) + if (fpclassify(Double_val(accu)) == FP_INFINITE) { + f = Double_val(accu); + } else +#endif f = frexp(Double_val(accu), &exp); if (fpclassify(f) == FP_NORMAL) { exp += FLOAT_EXP_SHIFT; diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index f67119020e..668a55977d 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -4,9 +4,9 @@ : float (-2.5)%float : float -2.5e+20%float +2.4999999999999999e+123%float : float -(-2.4999999999999999e-20)%float +(-2.5000000000000001e-123)%float : float (2 + 2)%float : float @@ -18,9 +18,9 @@ : float -2.5 : float -2.5e+20 +2.4999999999999999e+123 : float --2.4999999999999999e-20 +-2.5000000000000001e-123 : float 2 + 2 : float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 1caa0bb444..85f611352c 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -3,8 +3,11 @@ Require Import Floats. Check 2%float. Check 2.5%float. Check (-2.5)%float. -Check 2.5e20%float. -Check (-2.5e-20)%float. +(* Avoid exponents with less than three digits as they are usually + displayed with two digits (1e7 is displayed 1e+07) except on + Windows where three digits are used (1e+007). *) +Check 2.5e123%float. +Check (-2.5e-123)%float. Check (2 + 2)%float. Check (2.5 + 2.5)%float. @@ -13,8 +16,8 @@ Open Scope float_scope. Check 2. Check 2.5. Check (-2.5). -Check 2.5e20. -Check (-2.5e-20). +Check 2.5e123. +Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). |