From 2cd34be6bf7ff2744ab7cdfa176d5423bacb4d13 Mon Sep 17 00:00:00 2001
From: vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4>
Date: Mon, 4 Feb 2019 13:23:37 +0000
Subject: [tools/mpfrlint] Check that native FP division by zero is not used.

git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@13441 280ebfd0-de03-0410-8827-d642c229c3f4
---
 tools/mpfrlint | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tools')

diff --git a/tools/mpfrlint b/tools/mpfrlint
index 7aae5403c..454ec3184 100755
--- a/tools/mpfrlint
+++ b/tools/mpfrlint
@@ -362,6 +362,10 @@ err-if-output \
   -t "mpfr-impl.h inclusion" grep --exclude=mpfr-test.h \
     '^ *# *include *"mpfr-impl.h"' tests/*.{c,h}
 
+grep -E '/ *0?\.0([^0-9]|$)' tests/*.{c,h} | \
+  err-if-output --msg='division by zero yields issues on some platforms' \
+                -t "division by zero" grep -Ev '/\*.*/ *0?\.0'
+
 # Check that the usual test programs call tests_start_mpfr and tests_end_mpfr.
 if grep -q TESTS_NO_TVERSION tests/Makefile.am; then
   tprgvar=TESTS_NO_TVERSION
-- 
cgit v1.2.1