1 files changed, 9 insertions, 0 deletions
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/.*=//