[doc/README.dev] Improved description of MPFR_ERRDIVZERO.

[tools/mpfrlint] Check that native FP division by zero is not used.
(merged changesets r13441-13443 from the trunk)

git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/branches/4.0@13447 280ebfd0-de03-0410-8827-d642c229c3f4

2 files changed, 16 insertions, 4 deletions

diff --git a/doc/README.dev b/doc/README.dev
index 1b014afff..d79635cd5 100644
--- a/doc/README.dev
+++ b/doc/README.dev
@@ -506,10 +506,13 @@ List of macros used for checking MPFR:
 + HAVE_GETTIMEOFDAY:    Define if the function gettimeofday() is available.
 + HAVE_SETLOCALE:       Define if the function setlocale() is available.
 + MPFR_ERRDIVZERO:      Define if the floating-point division by 0 fails
-                        (e.g. because a SIGFPE signal is generated, or
-                        because it is regarded as undefined behavior by
-                        a sanitizer). This disables the tests involving
-                        such operations.
+                        in the MPFR library (e.g., because a SIGFPE signal
+                        is generated, or because it is regarded as undefined
+                        behavior by a sanitizer). This disables the tests
+                        involving such operations.
+                        Note: Tests related to NaN and infinities must not
+                        rely on native FP division by 0, whether this macro
+                        is defined or not.
 + MPFR_TESTS_FPE_DIV:   Define to check whether there has been a FP
                         exception FE_DIVBYZERO or FE_INVALID, which
                         probably comes from 1.0 / 0.0 or 0.0 / 0.0 to
diff --git a/tools/mpfrlint b/tools/mpfrlint
index 04fc8a9f2..0a42508a6 100755
--- a/tools/mpfrlint
+++ b/tools/mpfrlint
@@ -336,6 +336,15 @@ err-if-output \
   -t "mpfr-impl.h inclusion" grep --exclude=mpfr-test.h \
     '^ *# *include *"mpfr-impl.h"' tests/*.{c,h}
 
+# Division by zero yields issues on some platforms, even in the case where
+# MPFR_ERRDIVZERO is not defined. See, e.g.
+#   https://sympa.inria.fr/sympa/arc/mpfr/2019-02/msg00005.html
+# The solution is to still allow tests related to NaN and infinities, but
+# such tests must avoid division by zero.
+grep -E '/ *0?\.0([^0-9]|$)' tests/*.{c,h} | \
+  err-if-output --msg='Division by zero yields issues on some platforms, use MPFR_DBL_* macros.' \
+                -t "division by zero" grep -Ev '/\*.*/ *0?\.0'
+
 # Check that the usual test programs call tests_start_mpfr and tests_end_mpfr.
 tprg=($(sed -n '/^check_PROGRAMS/,/[^\\]$/ {
   s/.*=//