[PPL-devel] [GIT] ppl/ppl(master): INT_MIN % -1 is undefined behavior in C++11.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: ccd09e698f00e26a8dc4ccc2265843e6b9ec1598
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ccd09e698f00e26a8dc4ccc2265843e6b9ec1598

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sat Feb 11 20:51:31 2012 +0100

INT_MIN % -1 is undefined behavior in C++11.
The PPL has been proven to be immune to this potential problem by ECLAIR.
(Thanks to Rene Sugar.)

---

 TODO                       |    7 ----
 configure.ac               |    5 +--
 m4/ac_cxx_remainder_bug.m4 |   71 --------------------------------------------
 src/checked.cc             |    1 +
 4 files changed, 2 insertions(+), 82 deletions(-)

diff --git a/TODO b/TODO
index 6ea8729..271fb42 100644
--- a/TODO
+++ b/TODO
@@ -23,13 +23,6 @@ Enhancements for PPL 0.12 or later versions
   Explain it in README.configure.
 - Ensure the tests in tests/MIP_Problem/* cover every line of
   code in MIP_Problem.*.
-- Define functions rem() and remp() to compute the remainder of division
-  in the general case, for rem(), and in the case where the second
-  argument is known to be positive, for remp().  In the implementation
-  of rem(), if CXX_HAS_REMAINDER_BUG is nonzero, a suitable workaround
-  should be implemented to circumvent the INT_MIN % -1 bug.
-  rem() and remp() should be used (with a strong preference to the second,
-  of course) wherever we now use operator%().
 - Suppose we want to sum three numbers, and suppose we do it by
 
     add(T& to, const T& x, const T& y, const T& z) {
diff --git a/configure.ac b/configure.ac
index 898f540..eed647d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -24,7 +24,7 @@
 # Process this file with Autoconf to produce a configure script.
 
 # Every other copy of the package version number gets its value from here.
-AC_INIT([the Parma Polyhedra Library], [0.12pre3], [ppl-devel at cs.unipr.it], [ppl])
+AC_INIT([the Parma Polyhedra Library], [0.12pre4], [ppl-devel at cs.unipr.it], [ppl])
 
 # Minimum Autoconf version required.
 AC_PREREQ(2.61)
@@ -780,9 +780,6 @@ AC_CXX_SUPPORTS_ZERO_LENGTH_ARRAYS
 # Check whether the IEEE inexact flag is supported in C++.
 AC_CXX_SUPPORTS_IEEE_INEXACT_FLAG
 
-# Check whether the C++ compiler has the remainder bug.
-AC_CXX_HAS_REMAINDER_BUG
-
 # Check whether the C++ compiler supports __attribute__ ((weak)).
 AC_CXX_SUPPORTS_ATTRIBUTE_WEAK
 
diff --git a/m4/ac_cxx_remainder_bug.m4 b/m4/ac_cxx_remainder_bug.m4
deleted file mode 100644
index 0dfb146..0000000
--- a/m4/ac_cxx_remainder_bug.m4
+++ /dev/null
@@ -1,71 +0,0 @@
-dnl A function to check whether the C++ compiler has the `remainder' bug.
-dnl Copyright (C) 2001-2010 Roberto Bagnara <bagnara at cs.unipr.it>
-dnl Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com)
-dnl
-dnl This file is part of the Parma Polyhedra Library (PPL).
-dnl
-dnl The PPL is free software; you can redistribute it and/or modify it
-dnl under the terms of the GNU General Public License as published by the
-dnl Free Software Foundation; either version 3 of the License, or (at your
-dnl option) any later version.
-dnl
-dnl The PPL is distributed in the hope that it will be useful, but WITHOUT
-dnl ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
-dnl FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
-dnl for more details.
-dnl
-dnl You should have received a copy of the GNU General Public License
-dnl along with this program; if not, write to the Free Software Foundation,
-dnl Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
-dnl
-dnl For the most up-to-date information see the Parma Polyhedra Library
-dnl site: http://bugseng.com/products/ppl/ .
-
-AC_DEFUN([AC_CXX_HAS_REMAINDER_BUG],
-[
-
-ac_save_CPPFLAGS="$CPPFLAGS"
-ac_save_LIBS="$LIBS"
-AC_LANG_PUSH(C++)
-
-AC_MSG_CHECKING([if the compiler has the remainder bug])
-AC_RUN_IFELSE([AC_LANG_SOURCE([[
-#include <climits>
-
-int minus_one(int n) {
-  return (n+1)*(n-1)-n*n;
-}
-
-int p(int x, int y) {
-  int z = x % y;
-  return z;
-}
-
-int main(int argc, char** argv) {
-  if (p(INT_MIN, minus_one(argc)) != 0)
-    return 1;
-  else
-    return 0;
-}
-]])],
-  AC_MSG_RESULT(no)
-  ac_cv_cxx_has_remainder_bug=no,
-  AC_MSG_RESULT(yes)
-  ac_cv_cxx_has_remainder_bug=yes,
-  AC_MSG_RESULT([assuming yes])
-  ac_cv_cxx_has_remainder_bug=yes)
-
-if test x"$ac_cv_cxx_has_remainder_bug" = xyes
-then
-  value=1
-else
-  value=0
-fi
-AC_DEFINE_UNQUOTED(PPL_CXX_HAS_REMAINDER_BUG, $value,
-  [Not zero if the C++ compiler has the remainder bug.])
-
-AC_LANG_POP(C++)
-CPPFLAGS="$ac_save_CPPFLAGS"
-LIBS="$ac_save_LIBS"
-])
-
diff --git a/src/checked.cc b/src/checked.cc
index 104fecf..93a933c 100644
--- a/src/checked.cc
+++ b/src/checked.cc
@@ -278,6 +278,7 @@ parse_number_part(std::istream& is, number_struct& numer) {
           goto unexpected;
       exp:
         state = EXPONENT;
+        PPL_ASSERT(numer.base >= 2);
         max_exp_div = LONG_MAX / numer.base;
         max_exp_rem = static_cast<int>(LONG_MAX % numer.base);
         if (!is.get(c))