summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Assert.cpp101
-rw-r--r--src/util/Assert.h189
-rw-r--r--src/util/Makefile.am16
-rw-r--r--src/util/Makefile.in29
-rw-r--r--src/util/exception.h12
5 files changed, 262 insertions, 85 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
new file mode 100644
index 000000000..799af12ab
--- /dev/null
+++ b/src/util/Assert.cpp
@@ -0,0 +1,101 @@
+/********************* -*- C++ -*- */
+/** Assert.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Assertion utility classes, functions, and exceptions. Implementation.
+ **/
+
+#include <new>
+#include <cstdarg>
+#include <cstdio>
+#include "util/Assert.h"
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+void AssertionException::construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt,
+ va_list args) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 256;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
+ header, function, file, line);
+ } else {
+ size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n",
+ header, function, file, line, extra);
+ }
+
+ if(size < n) {
+ va_list args_copy;
+ va_copy(args_copy, args);
+ size += vsnprintf(buf + size, n - size, fmt, args);
+ va_end(args_copy);
+
+ if(size < n) {
+ break;
+ }
+ }
+
+ if(size >= n) {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+ delete [] buf;
+}
+
+void AssertionException::construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 256;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
+ header, function, file, line);
+ } else {
+ size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n",
+ header, function, file, line, extra);
+ }
+
+ if(size < n) {
+ break;
+ } else {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+ delete [] buf;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 8fd970c6c..3da76c5db 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -1,5 +1,5 @@
/********************* -*- C++ -*- */
-/** assert.h
+/** Assert.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
@@ -7,13 +7,15 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** Assertion utility classes, functions, and exceptions.
+ ** Assertion utility classes, functions, exceptions, and macros.
**/
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
#include <string>
+#include <cstdio>
+#include <cstdarg>
#include "util/exception.h"
#include "cvc4_config.h"
#include "config.h"
@@ -21,91 +23,136 @@
namespace CVC4 {
class CVC4_PUBLIC AssertionException : public Exception {
-public:
+protected:
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, ...) {
+ va_list args;
+ va_start(args, fmt);
+ construct(header, extra, function, file, line, fmt, args);
+ va_end(args);
+ }
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, va_list args);
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line);
+
AssertionException() : Exception() {}
- AssertionException(std::string msg) : Exception(msg) {}
- AssertionException(const char* msg) : Exception(msg) {}
+
+public:
+ AssertionException(const char* extra, const char* function,
+ const char* file, unsigned line,
+ const char* fmt, ...) :
+ Exception() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Assertion failure", extra, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ AssertionException(const char* extra, const char* function,
+ const char* file, unsigned line) :
+ Exception() {
+ construct("Assertion failure", extra, function, file, line);
+ }
};/* class AssertionException */
class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
-public:
+protected:
UnreachableCodeException() : AssertionException() {}
- UnreachableCodeException(std::string msg) : AssertionException(msg) {}
- UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+
+public:
+ UnreachableCodeException(const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Unreachable code reached",
+ NULL, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ UnreachableCodeException(const char* function, const char* file,
+ unsigned line) :
+ AssertionException() {
+ construct("Unreachable code reached", NULL, function, file, line);
+ }
};/* class UnreachableCodeException */
class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
-public:
+protected:
UnhandledCaseException() : UnreachableCodeException() {}
- UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
- UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+
+public:
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ UnreachableCodeException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Unhandled case encountered",
+ NULL, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line, int theCase) :
+ UnreachableCodeException() {
+ construct("Unhandled case encountered",
+ NULL, function, file, line, "The case was: %d", theCase);
+ }
+
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line) :
+ UnreachableCodeException() {
+ construct("Unhandled case encountered", NULL, function, file, line);
+ }
};/* class UnhandledCaseException */
+class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
+protected:
+ IllegalArgumentException() : AssertionException() {}
+
+public:
+ IllegalArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line,
+ const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Illegal argument detected",
+ argDesc, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ IllegalArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line) :
+ AssertionException() {
+ construct("Illegal argument detected",
+ argDesc, function, file, line);
+ }
+};/* class IllegalArgumentException */
+
+#define AlwaysAssert(cond, msg...) \
+ do { \
+ if(EXPECT_FALSE( ! (cond) )) { \
+ throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \
+ } \
+ } while(0)
+#define Unreachable(msg...) \
+ throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unhandled(msg...) \
+ throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define IllegalArgument(arg, msg...) \
+ throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg)
+
#ifdef CVC4_ASSERTIONS
-# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
+# define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
#else /* ! CVC4_ASSERTIONS */
# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
#endif /* CVC4_ASSERTIONS */
-#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
-#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
-
-#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
-#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
-
-inline void AssertImpl(const char* info, bool cond, std::string msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond, const char* msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(info);
-}
-
-#ifdef __GNUC__
-inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnreachableImpl(const char* info, std::string msg) {
- throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info, const char* msg) {
- throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info) {
- throw UnreachableCodeException(info);
-}
-
-#ifdef __GNUC__
-inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnhandledImpl(const char* info, std::string msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info, const char* msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info) {
- throw UnhandledCaseException(info);
-}
-
}/* CVC4 namespace */
#endif /* __CVC4__ASSERT_H */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 8baf872d2..b6c116a6d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -5,6 +5,20 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
+ Assert.h \
+ Assert.cpp \
+ Makefile.am \
+ Makefile.in \
command.cpp \
+ command.h \
+ debug.h \
decision_engine.cpp \
- output.cpp
+ decision_engine.h \
+ exception.h \
+ literal.h \
+ model.h \
+ options.h \
+ output.cpp \
+ output.h \
+ result.h \
+ unique_id.h
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index ac8d4b522..9f17df4c7 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -52,7 +52,8 @@ CONFIG_CLEAN_FILES =
CONFIG_CLEAN_VPATH_FILES =
LTLIBRARIES = $(noinst_LTLIBRARIES)
libutil_la_LIBADD =
-am_libutil_la_OBJECTS = command.lo decision_engine.lo output.lo
+am_libutil_la_OBJECTS = Assert.lo command.lo decision_engine.lo \
+ output.lo
libutil_la_OBJECTS = $(am_libutil_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -67,6 +68,15 @@ CXXLD = $(CXX)
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libutil_la_SOURCES)
DIST_SOURCES = $(libutil_la_SOURCES)
ETAGS = etags
@@ -211,9 +221,23 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
+ Assert.h \
+ Assert.cpp \
+ Makefile.am \
+ Makefile.in \
command.cpp \
+ command.h \
+ debug.h \
decision_engine.cpp \
- output.cpp
+ decision_engine.h \
+ exception.h \
+ literal.h \
+ model.h \
+ options.h \
+ output.cpp \
+ output.h \
+ result.h \
+ unique_id.h
all: all-am
@@ -267,6 +291,7 @@ mostlyclean-compile:
distclean-compile:
-rm -f *.tab.c
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/Assert.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/command.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/decision_engine.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/output.Plo@am__quote@
diff --git a/src/util/exception.h b/src/util/exception.h
index 164cda8b5..d239f48de 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -31,7 +31,7 @@ public:
Exception(const char* msg) : d_msg(msg) {}
// Destructor
virtual ~Exception() {}
- // NON-VIRTUAL METHODs for setting and printing the error message
+ // NON-VIRTUAL METHOD for setting and printing the error message
void setMessage(const std::string& msg) { d_msg = msg; }
// Printing: feel free to redefine toString(). When inherited,
// it's recommended that this method print the type of exception
@@ -41,20 +41,10 @@ public:
friend std::ostream& operator<<(std::ostream& os, const Exception& e);
};/* class Exception */
-
-class CVC4_PUBLIC IllegalArgumentException : public Exception {
-public:
- IllegalArgumentException() : Exception("Illegal argument to method or function") {}
- IllegalArgumentException(const std::string& msg) : Exception(msg) {}
- IllegalArgumentException(const char* msg) : Exception(msg) {}
-};/* class IllegalArgumentException */
-
-
inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
return os << e.toString();
}
-
}/* CVC4 namespace */
#endif /* __CVC4__EXCEPTION_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback