[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): New policy Debug_WRD_Extended_Number_Policy.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Thu May 14 08:30:18 2009 +0200

New policy Debug_WRD_Extended_Number_Policy.
This is the debugging policy for checked numbers used in weakly-relational
domains.

---

 src/BD_Shape.defs.hh                 |    2 +-
 src/Octagonal_Shape.defs.hh          |    2 +-
 src/WRD_coefficient_types.defs.hh    |   71 +++++++++++++++++++++++++++++++++-
 src/WRD_coefficient_types.inlines.hh |    6 +++
 4 files changed, 78 insertions(+), 3 deletions(-)

diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh
index a15ff6a..f836ad7 100644
--- a/src/BD_Shape.defs.hh
+++ b/src/BD_Shape.defs.hh
@@ -406,7 +406,7 @@ private:
     the inequalities defining a BDS.
   */
 #ifndef NDEBUG
-  typedef Checked_Number<T, Extended_Number_Policy> N;
+  typedef Checked_Number<T, Debug_WRD_Extended_Number_Policy> N;
 #else
   typedef Checked_Number<T, WRD_Extended_Number_Policy> N;
 #endif
diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index 02bbb32..f227261 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -417,7 +417,7 @@ private:
     the inequalities defining an OS.
   */
 #ifndef NDEBUG
-  typedef Checked_Number<T, Extended_Number_Policy> N;
+  typedef Checked_Number<T, Debug_WRD_Extended_Number_Policy> N;
 #else
   typedef Checked_Number<T, WRD_Extended_Number_Policy> N;
 #endif
diff --git a/src/WRD_coefficient_types.defs.hh b/src/WRD_coefficient_types.defs.hh
index ae7d707..1916c46 100644
--- a/src/WRD_coefficient_types.defs.hh
+++ b/src/WRD_coefficient_types.defs.hh
@@ -28,7 +28,12 @@ site: http://www.cs.unipr.it/ppl/ . */
 namespace Parma_Polyhedra_Library {
 
 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
-/*! \ingroup PPL_CXX_interface */
+/*! \brief
+  The production policy for checked numbers used in weakly-relational
+  domains.
+
+  \ingroup PPL_CXX_interface
+ */
 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
 struct WRD_Extended_Number_Policy {
   //! Check for overflowed result.
@@ -86,6 +91,70 @@ struct WRD_Extended_Number_Policy {
   static void handle_result(Result r);
 };
 
+#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
+/*! \brief
+  The debugging policy for checked numbers used in weakly-relational
+  domains.
+
+  \ingroup PPL_CXX_interface
+ */
+#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
+struct Debug_WRD_Extended_Number_Policy {
+  //! Check for overflowed result.
+  const_bool_nodef(check_overflow, true);
+
+  //! Check for attempts to add infinities with different sign.
+  const_bool_nodef(check_inf_add_inf, true);
+
+  //! Check for attempts to subtract infinities with same sign.
+  const_bool_nodef(check_inf_sub_inf, true);
+
+  //! Check for attempts to multiply infinities by zero.
+  const_bool_nodef(check_inf_mul_zero, true);
+
+  //! Check for attempts to divide by zero.
+  const_bool_nodef(check_div_zero, true);
+
+  //! Check for attempts to divide infinities.
+  const_bool_nodef(check_inf_div_inf, true);
+
+  //! Check for attempts to compute remainder of infinities.
+  const_bool_nodef(check_inf_mod, true);
+
+  //! Checks for attempts to take the square root of a negative number.
+  const_bool_nodef(check_sqrt_neg, true);
+
+  //! Handle not-a-number special value.
+  const_bool_nodef(has_nan, true);
+
+  //! Handle infinity special values.
+  const_bool_nodef(has_infinity, true);
+
+  // Do not uncomment the following.
+  // The compile time error on conversions is the expected behavior.
+  // const_bool_nodef(convertible, false);
+
+  //! Honor requests to check for FPU inexact results.
+  const_bool_nodef(fpu_check_inexact, true);
+
+  //! Make extra checks to detect FPU NaN results.
+  const_bool_nodef(fpu_check_nan_result, true);
+
+  // Do not uncomment the following.
+  // The compile time error is the expected behavior.
+  // static const Rounding_Dir ROUND_DEFAULT_CONSTRUCTOR = ROUND_UP;
+  // static const Rounding_Dir ROUND_DEFAULT_OPERATOR = ROUND_UP;
+  // static const Rounding_Dir ROUND_DEFAULT_FUNCTION = ROUND_UP;
+  // static const Rounding_Dir ROUND_DEFAULT_INPUT = ROUND_UP;
+  // static const Rounding_Dir ROUND_DEFAULT_OUTPUT = ROUND_UP;
+
+  /*! \brief
+    Handles \p r: called by all constructors, operators and functions that
+    do not return a Result value.
+  */
+  static void handle_result(Result r);
+};
+
 } // namespace Parma_Polyhedra_Library
 
 #include "WRD_coefficient_types.inlines.hh"
diff --git a/src/WRD_coefficient_types.inlines.hh b/src/WRD_coefficient_types.inlines.hh
index 2f98f58..0bcd080 100644
--- a/src/WRD_coefficient_types.inlines.hh
+++ b/src/WRD_coefficient_types.inlines.hh
@@ -31,6 +31,12 @@ WRD_Extended_Number_Policy::handle_result(Result r) {
     throw_result_exception(r);
 }
 
+inline void
+Debug_WRD_Extended_Number_Policy::handle_result(Result r) {
+  if (result_class(r) == VC_NAN)
+    throw_result_exception(r);
+}
+
 } // namespace Parma_Polyhedra_Library
 
 #endif // !defined(PPL_WRD_coefficient_types_inlines_hh)