src/util/Assert.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** Assert.h
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Assertion utility classes, functions, exceptions, and macros.
  11  **/
  12
  13 #ifndef __CVC4__ASSERT_H
  14 #define __CVC4__ASSERT_H
  15
  16 #include <string>
  17 #include <cstdio>
  18 #include <cstdarg>
  19 #include "util/exception.h"
  20 #include "cvc4_config.h"
  21 #include "config.h"
  22
  23 namespace CVC4 {
  24
  25 class CVC4_PUBLIC AssertionException : public Exception {
  26 protected:
  27   void construct(const char* header, const char* extra,
  28                  const char* function, const char* file,
  29                  unsigned line, const char* fmt, ...) {
  30     va_list args;
  31     va_start(args, fmt);
  32     construct(header, extra, function, file, line, fmt, args);
  33     va_end(args);
  34   }
  35   void construct(const char* header, const char* extra,
  36                  const char* function, const char* file,
  37                  unsigned line, const char* fmt, va_list args);
  38   void construct(const char* header, const char* extra,
  39                  const char* function, const char* file,
  40                  unsigned line);
  41
  42   AssertionException() : Exception() {}
  43
  44 public:
  45   AssertionException(const char* extra, const char* function,
  46                      const char* file, unsigned line,
  47                      const char* fmt, ...) :
  48     Exception() {
  49     va_list args;
  50     va_start(args, fmt);
  51     construct("Assertion failure", extra, function, file, line, fmt, args);
  52     va_end(args);
  53   }
  54
  55   AssertionException(const char* extra, const char* function,
  56                      const char* file, unsigned line) :
  57     Exception() {
  58     construct("Assertion failure", extra, function, file, line);
  59   }
  60 };/* class AssertionException */
  61
  62 class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
  63 protected:
  64   UnreachableCodeException() : AssertionException() {}
  65
  66 public:
  67   UnreachableCodeException(const char* function, const char* file,
  68                            unsigned line, const char* fmt, ...) :
  69     AssertionException() {
  70     va_list args;
  71     va_start(args, fmt);
  72     construct("Unreachable code reached",
  73               NULL, function, file, line, fmt, args);
  74     va_end(args);
  75   }
  76
  77   UnreachableCodeException(const char* function, const char* file,
  78                            unsigned line) :
  79     AssertionException() {
  80     construct("Unreachable code reached", NULL, function, file, line);
  81   }
  82 };/* class UnreachableCodeException */
  83
  84 class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
  85 protected:
  86   UnhandledCaseException() : UnreachableCodeException() {}
  87
  88 public:
  89   UnhandledCaseException(const char* function, const char* file,
  90                          unsigned line, const char* fmt, ...) :
  91     UnreachableCodeException() {
  92     va_list args;
  93     va_start(args, fmt);
  94     construct("Unhandled case encountered",
  95               NULL, function, file, line, fmt, args);
  96     va_end(args);
  97   }
  98
  99   UnhandledCaseException(const char* function, const char* file,
 100                          unsigned line, int theCase) :
 101     UnreachableCodeException() {
 102     construct("Unhandled case encountered",
 103               NULL, function, file, line, "The case was: %d", theCase);
 104   }
 105
 106   UnhandledCaseException(const char* function, const char* file,
 107                          unsigned line) :
 108     UnreachableCodeException() {
 109     construct("Unhandled case encountered", NULL, function, file, line);
 110   }
 111 };/* class UnhandledCaseException */
 112
 113 class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
 114 protected:
 115   IllegalArgumentException() : AssertionException() {}
 116
 117 public:
 118   IllegalArgumentException(const char* argDesc, const char* function,
 119                            const char* file, unsigned line,
 120                            const char* fmt, ...) :
 121     AssertionException() {
 122     va_list args;
 123     va_start(args, fmt);
 124     construct("Illegal argument detected",
 125               argDesc, function, file, line, fmt, args);
 126     va_end(args);
 127   }
 128
 129   IllegalArgumentException(const char* argDesc, const char* function,
 130                            const char* file, unsigned line) :
 131     AssertionException() {
 132     construct("Illegal argument detected",
 133               argDesc, function, file, line);
 134   }
 135 };/* class IllegalArgumentException */
 136
 137 #define AlwaysAssert(cond, msg...) \
 138   do { \
 139     if(EXPECT_FALSE( ! (cond) )) { \
 140       throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
 141     } \
 142   } while(0)
 143 #define Unreachable(msg...) \
 144   throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 145 #define Unhandled(msg...) \
 146   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 147 #define IllegalArgument(arg, msg...) \
 148   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 149
 150 #ifdef CVC4_ASSERTIONS
 151 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
 152 #else /* ! CVC4_ASSERTIONS */
 153 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
 154 #endif /* CVC4_ASSERTIONS */
 155
 156 }/* CVC4 namespace */
 157
 158 #endif /* __CVC4__ASSERT_H */