[PPL-devel] [GIT] ppl/ppl(master): Added functions ppl_unreachable() and ppl_unreachable_msg(),
Enea Zaffanella
zaffanella at cs.unipr.it
Sat Dec 10 12:55:55 CET 2011
Module: ppl/ppl
Branch: master
Commit: 5d56513b2dc23fae0bc40c822299f2cfc18dad35
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d56513b2dc23fae0bc40c822299f2cfc18dad35
Author: Enea Zaffanella <zaffanella at cs.unipr.it>
Date: Sat Dec 10 12:50:48 2011 +0100
Added functions ppl_unreachable() and ppl_unreachable_msg(),
causing program termination using abort().
Let PPL_UNREACHABLE and PPL_ASSERT be based on these functions.
Avoid a cycle in header inclusion dependencies.
---
doc/devref.doxyconf-html.in | 2 +
doc/devref.doxyconf-latex.in | 2 +
src/Makefile.am | 1 +
src/Partial_Function.inlines.hh | 2 +-
src/assert.cc | 44 +++++++++++++++++++
src/assert.hh | 91 +++++++++++++++++++++++++++------------
src/checked.defs.hh | 1 +
src/globals.inlines.hh | 2 +-
8 files changed, 115 insertions(+), 30 deletions(-)
diff --git a/doc/devref.doxyconf-html.in b/doc/devref.doxyconf-html.in
index ea929aa..33619fd 100644
--- a/doc/devref.doxyconf-html.in
+++ b/doc/devref.doxyconf-html.in
@@ -92,6 +92,8 @@ INPUT = @srcdir@/definitions.dox \
../src/version.hh \
@srcdir@/../src/version.cc \
@srcdir@/../src/meta_programming.hh \
+ @srcdir@/../src/assert.hh \
+ @srcdir@/../src/assert.cc \
@srcdir@/../src/Float.defs.hh \
@srcdir@/../src/Float.inlines.hh \
@srcdir@/../src/Float.cc \
diff --git a/doc/devref.doxyconf-latex.in b/doc/devref.doxyconf-latex.in
index 1c75de1..7521241 100644
--- a/doc/devref.doxyconf-latex.in
+++ b/doc/devref.doxyconf-latex.in
@@ -92,6 +92,8 @@ INPUT = @srcdir@/definitions.dox \
../src/version.hh \
@srcdir@/../src/version.cc \
@srcdir@/../src/meta_programming.hh \
+ @srcdir@/../src/assert.hh \
+ @srcdir@/../src/assert.cc \
@srcdir@/../src/Float.defs.hh \
@srcdir@/../src/Float.inlines.hh \
@srcdir@/../src/Float.cc \
diff --git a/src/Makefile.am b/src/Makefile.am
index be1d931..1e488e7 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -431,6 +431,7 @@ BDS_Status.idefs.hh \
Og_Status.idefs.hh
libppl_la_SOURCES = \
+assert.cc \
Box.cc \
checked.cc \
Checked_Number.cc \
diff --git a/src/Partial_Function.inlines.hh b/src/Partial_Function.inlines.hh
index 1ca05fb..212088b 100644
--- a/src/Partial_Function.inlines.hh
+++ b/src/Partial_Function.inlines.hh
@@ -25,7 +25,7 @@ site: http://bugseng.com/products/ppl/ . */
#define PPL_Partial_Function_inlines_hh 1
#include <stdexcept>
-#include <cassert>
+#include "assert.hh"
namespace Parma_Polyhedra_Library {
diff --git a/src/assert.cc b/src/assert.cc
new file mode 100644
index 0000000..2a951a4
--- /dev/null
+++ b/src/assert.cc
@@ -0,0 +1,44 @@
+/* Definitions of assert-like functions.
+ Copyright (C) 2001-2010 Roberto Bagnara <bagnara at cs.unipr.it>
+ Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com)
+
+This file is part of the Parma Polyhedra Library (PPL).
+
+The PPL is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by the
+Free Software Foundation; either version 3 of the License, or (at your
+option) any later version.
+
+The PPL is distributed in the hope that it will be useful, but WITHOUT
+ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program; if not, write to the Free Software Foundation,
+Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
+
+For the most up-to-date information see the Parma Polyhedra Library
+site: http://bugseng.com/products/ppl/ . */
+
+#include "ppl-config.h"
+#include "assert.hh"
+#include <cstdlib>
+#include <iostream>
+
+namespace PPL = Parma_Polyhedra_Library;
+
+void
+PPL::ppl_unreachable() {
+ abort();
+}
+
+void
+PPL::ppl_unreachable_msg(const char* msg,
+ const char* file, unsigned int line,
+ const char* function) {
+ std::cerr << "Aborting PPL computation!\n";
+ std::cerr << file << ":" << line << ": " << function << ": " << msg << "\n";
+ abort();
+}
+
diff --git a/src/assert.hh b/src/assert.hh
index f480f10..277fd07 100644
--- a/src/assert.hh
+++ b/src/assert.hh
@@ -1,4 +1,4 @@
-/* Implementation of PPL_ASSERT macro.
+/* Implementation of PPL assert-like macros.
Copyright (C) 2001-2010 Roberto Bagnara <bagnara at cs.unipr.it>
Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com)
@@ -24,55 +24,90 @@ site: http://bugseng.com/products/ppl/ . */
#ifndef PPL_assert_hh
#define PPL_assert_hh 1
-#include <cassert>
#include "globals.defs.hh"
+// The PPL_UNREACHABLE_MSG macro flags a program point as unreachable.
+// Argument `msg__' is added to output when assertions are turned on.
#if defined(NDEBUG)
+#define PPL_UNREACHABLE_MSG(msg__) Parma_Polyhedra_Library::ppl_unreachable()
+#else
+#define PPL_UNREACHABLE_MSG(msg__) Parma_Polyhedra_Library:: \
+ ppl_unreachable_msg(msg__, __FILE__, __LINE__, __func__)
+#endif
+
+// The PPL_UNREACHABLE macro flags a program point as unreachable.
+#define PPL_UNREACHABLE PPL_UNREACHABLE_MSG("unreachable")
-#define PPL_ASSERT(cond__)
-#define PPL_ASSERT_HEAVY(cond__)
-// Try to force a segmentation fault (volatile null pointer deref).
-#define PPL_UNREACHABLE (*(volatile int*)0)
+// Helper macro PPL_ASSERT_IMPL_: do not use it directly.
+#if defined(NDEBUG)
+#define PPL_ASSERT_IMPL_(cond__) ((void) 0)
#else
+#define PPL_STRING_(s) #s
+#define PPL_ASSERT_IMPL_(cond__) \
+ ((cond__) ? (void) 0 : PPL_UNREACHABLE_MSG(PPL_STRING_(cond__)))
+#endif
+
// Non zero to detect use of PPL_ASSERT instead of PPL_ASSERT_HEAVY
#define PPL_DEBUG_PPL_ASSERT 1
-#if !PPL_DEBUG_PPL_ASSERT
-#define PPL_ASSERT(cond__) assert(cond__)
+
+// The PPL_ASSERT macro states that Boolean condition cond__ should hold.
+// This is meant to replace uses of C assert().
+#if defined(NDEBUG) || (!PPL_DEBUG_PPL_ASSERT)
+#define PPL_ASSERT(cond__) PPL_ASSERT_IMPL_(cond__)
#else
-#define PPL_ASSERT(cond__) \
- do { \
- Parma_Polyhedra_Library::Weightwatch_Traits::Threshold \
- old_weight__ \
- = Parma_Polyhedra_Library::Weightwatch_Traits::weight; \
- assert(cond__); \
- assert(old_weight__ == Parma_Polyhedra_Library::Weightwatch_Traits::weight && \
- "PPL_ASSERT_HEAVY have to be used here"); \
+#define PPL_ASSERT(cond__) \
+ do { \
+ typedef Parma_Polyhedra_Library::Weightwatch_Traits W_Traits; \
+ W_Traits::Threshold old_weight__ = W_Traits::weight; \
+ PPL_ASSERT_IMPL_(cond__); \
+ PPL_ASSERT_IMPL_(old_weight__ == W_Traits::weight \
+ && "PPL_ASSERT_HEAVY have to be used here"); \
} while(0)
-#endif
+#endif // !defined(NDEBUG) && PPL_DEBUG_PPL_ASSERT
-// The evaluation of asserted conditions could have a non zero
-// computational weight (i.e., the execution path could contain an
-// invocation of WEIGHT_ADD).
-#define PPL_ASSERT_HEAVY(cond__) \
- do { \
- ++Parma_Polyhedra_Library::Implementation::in_assert; \
- assert(cond__); \
- --Parma_Polyhedra_Library::Implementation::in_assert; \
- } while (0)
-
-#define PPL_UNREACHABLE PPL_ASSERT(false)
+// Macro PPL_ASSERT_HEAVY is meant to be used when the evaluation of
+// the assertion may change computational weights (via WEIGHT_ADD).
+#if defined(NDEBUG)
+#define PPL_ASSERT_HEAVY(cond__) PPL_ASSERT_IMPL_(cond__)
+#else
+#define PPL_ASSERT_HEAVY(cond__) \
+ do { \
+ ++Parma_Polyhedra_Library::Implementation::in_assert; \
+ PPL_ASSERT_IMPL_(cond__); \
+ --Parma_Polyhedra_Library::Implementation::in_assert; \
+ } while (0)
#endif // !defined(NDEBUG)
+// Macro PPL_EXPECT (resp., PPL_EXPECT_HEAVY) should be used rather than
+// PPL_ASSERT (resp., PPL_ASSERT_HEAVY) when the condition is assumed to
+// hold but it is not under library control (typically, it depends on
+// user provided input).
+#define PPL_EXPECT(cond__) PPL_ASSERT(cond__)
#define PPL_EXPECT_HEAVY(cond__) PPL_ASSERT_HEAVY(cond__)
namespace Parma_Polyhedra_Library {
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
+//! Helper function causing program termination by calling \c abort.
+#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
+void ppl_unreachable() __attribute__((weak, noreturn));
+
+#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
+/*! \brief
+ Helper function printing message on \c std::cerr and causing program
+ termination by calling \c abort.
+*/
+#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
+void ppl_unreachable_msg(const char* msg,
+ const char* file, unsigned int line,
+ const char* function) __attribute__((weak, noreturn));
+
+#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
/*! \brief
Returns \c true if and only if \p x_copy contains \p y_copy.
diff --git a/src/checked.defs.hh b/src/checked.defs.hh
index 642d763..7434544 100644
--- a/src/checked.defs.hh
+++ b/src/checked.defs.hh
@@ -24,6 +24,7 @@ site: http://bugseng.com/products/ppl/ . */
#ifndef PPL_checked_defs_hh
#define PPL_checked_defs_hh 1
+#include <cassert>
#include <iostream>
#include <gmpxx.h>
#include "mp_std_bits.defs.hh"
diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh
index 6a72759..7098542 100644
--- a/src/globals.inlines.hh
+++ b/src/globals.inlines.hh
@@ -25,7 +25,7 @@ site: http://bugseng.com/products/ppl/ . */
#define PPL_globals_inlines_hh 1
#include <limits>
-#include "assert.hh"
+#include <cassert>
namespace Parma_Polyhedra_Library {
More information about the PPL-devel
mailing list