Module: ppl/ppl Branch: bounded_arithmetic Commit: e33e130ebcb92b6ae36fdd8bf75d0c7c7e1b0047 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e33e130ebcb92... Author: Roberto Bagnara <bagnara@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)