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, and exceptions.
  11  **/
  12
  13 #ifndef __CVC4__ASSERT_H
  14 #define __CVC4__ASSERT_H
  15
  16 #include <string>
  17 #include "util/exception.h"
  18 #include "cvc4_config.h"
  19 #include "config.h"
  20
  21 namespace CVC4 {
  22
  23 class CVC4_PUBLIC AssertionException : public Exception {
  24 public:
  25   AssertionException() : Exception() {}
  26   AssertionException(std::string msg) : Exception(msg) {}
  27   AssertionException(const char* msg) : Exception(msg) {}
  28 };/* class AssertionException */
  29
  30 class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
  31 public:
  32   UnreachableCodeException() : AssertionException() {}
  33   UnreachableCodeException(std::string msg) : AssertionException(msg) {}
  34   UnreachableCodeException(const char* msg) : AssertionException(msg) {}
  35 };/* class UnreachableCodeException */
  36
  37 class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
  38 public:
  39   UnhandledCaseException() : UnreachableCodeException() {}
  40   UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
  41   UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
  42 };/* class UnhandledCaseException */
  43
  44 #ifdef CVC4_ASSERTIONS
  45 #  define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
  46 #else /* ! CVC4_ASSERTIONS */
  47 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
  48 #endif /* CVC4_ASSERTIONS */
  49
  50 #define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
  51 #define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
  52 #define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
  53
  54 #define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
  55 #define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
  56 #define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
  57
  58 inline void AssertImpl(const char* info, bool cond, std::string msg) {
  59   if(EXPECT_FALSE( ! cond ))
  60     throw AssertionException(std::string(info) + "\n" + msg);
  61 }
  62
  63 inline void AssertImpl(const char* info, bool cond, const char* msg) {
  64   if(EXPECT_FALSE( ! cond ))
  65     throw AssertionException(std::string(info) + "\n" + msg);
  66 }
  67
  68 inline void AssertImpl(const char* info, bool cond) {
  69   if(EXPECT_FALSE( ! cond ))
  70     throw AssertionException(info);
  71 }
  72
  73 #ifdef __GNUC__
  74 inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
  75 inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
  76 inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
  77 #endif /* __GNUC__ */
  78
  79 inline void UnreachableImpl(const char* info, std::string msg) {
  80   throw UnreachableCodeException(std::string(info) + "\n" + msg);
  81 }
  82
  83 inline void UnreachableImpl(const char* info, const char* msg) {
  84   throw UnreachableCodeException(std::string(info) + "\n" + msg);
  85 }
  86
  87 inline void UnreachableImpl(const char* info) {
  88   throw UnreachableCodeException(info);
  89 }
  90
  91 #ifdef __GNUC__
  92 inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
  93 inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
  94 inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
  95 #endif /* __GNUC__ */
  96
  97 inline void UnhandledImpl(const char* info, std::string msg) {
  98   throw UnhandledCaseException(std::string(info) + "\n" + msg);
  99 }
 100
 101 inline void UnhandledImpl(const char* info, const char* msg) {
 102   throw UnhandledCaseException(std::string(info) + "\n" + msg);
 103 }
 104
 105 inline void UnhandledImpl(const char* info) {
 106   throw UnhandledCaseException(info);
 107 }
 108
 109 }/* CVC4 namespace */
 110
 111 #endif /* __CVC4__ASSERT_H */