src/base/check.cpp

   1 /*********************                                                        */
   2 /*! \file check.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Assertion utility classes, functions and macros.
  13  **
  14  ** Implementation of assertion utility classes, functions and macros.
  15  **/
  16
  17 #include "base/check.h"
  18
  19 #include <cstdlib>
  20 #include <iostream>
  21
  22 namespace CVC4 {
  23
  24 FatalStream::FatalStream(const char* function, const char* file, int line)
  25 {
  26   stream() << "Fatal failure within " << function << " at " << file << ":"
  27            << line << "\n";
  28 }
  29
  30 FatalStream::~FatalStream()
  31 {
  32   Flush();
  33   abort();
  34 }
  35
  36 std::ostream& FatalStream::stream() { return std::cerr; }
  37
  38 void FatalStream::Flush()
  39 {
  40   stream() << std::endl;
  41   stream().flush();
  42 }
  43
  44 void AssertArgumentException::construct(const char* header,
  45                                         const char* extra,
  46                                         const char* function,
  47                                         const char* file,
  48                                         unsigned line,
  49                                         const char* fmt,
  50                                         va_list args)
  51 {
  52   // try building the exception msg with a smallish buffer first,
  53   // then with a larger one if sprintf tells us to.
  54   int n = 512;
  55   char* buf;
  56   buf = new char[n];
  57
  58   for (;;)
  59   {
  60     int size;
  61     if (extra == NULL)
  62     {
  63       size = snprintf(buf, n, "%s\n%s\n%s:%d\n", header, function, file, line);
  64     }
  65     else
  66     {
  67       size = snprintf(buf,
  68                       n,
  69                       "%s\n%s\n%s:%d:\n\n  %s\n",
  70                       header,
  71                       function,
  72                       file,
  73                       line,
  74                       extra);
  75     }
  76
  77     if (size < n)
  78     {
  79       va_list args_copy;
  80       va_copy(args_copy, args);
  81       size += vsnprintf(buf + size, n - size, fmt, args_copy);
  82       va_end(args_copy);
  83
  84       if (size < n)
  85       {
  86         break;
  87       }
  88     }
  89
  90     if (size >= n)
  91     {
  92       // try again with a buffer that's large enough
  93       n = size + 1;
  94       delete[] buf;
  95       buf = new char[n];
  96     }
  97   }
  98
  99   setMessage(std::string(buf));
 100
 101 #ifdef CVC4_DEBUG
 102   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
 103   if (buffer != NULL)
 104   {
 105     if (buffer->getContents() == NULL)
 106     {
 107       buffer->setContents(buf);
 108     }
 109   }
 110 #endif /* CVC4_DEBUG */
 111   delete[] buf;
 112 }
 113
 114 void AssertArgumentException::construct(const char* header,
 115                                         const char* extra,
 116                                         const char* function,
 117                                         const char* file,
 118                                         unsigned line)
 119 {
 120   // try building the exception msg with a smallish buffer first,
 121   // then with a larger one if sprintf tells us to.
 122   int n = 256;
 123   char* buf;
 124
 125   for (;;)
 126   {
 127     buf = new char[n];
 128
 129     int size;
 130     if (extra == NULL)
 131     {
 132       size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", header, function, file, line);
 133     }
 134     else
 135     {
 136       size = snprintf(buf,
 137                       n,
 138                       "%s.\n%s\n%s:%d:\n\n  %s\n",
 139                       header,
 140                       function,
 141                       file,
 142                       line,
 143                       extra);
 144     }
 145
 146     if (size < n)
 147     {
 148       break;
 149     }
 150     else
 151     {
 152       // try again with a buffer that's large enough
 153       n = size + 1;
 154       delete[] buf;
 155     }
 156   }
 157
 158   setMessage(std::string(buf));
 159
 160 #ifdef CVC4_DEBUG
 161   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
 162   if (buffer != NULL)
 163   {
 164     if (buffer->getContents() == NULL)
 165     {
 166       buffer->setContents(buf);
 167     }
 168   }
 169 #endif /* CVC4_DEBUG */
 170   delete[] buf;
 171 }
 172
 173 AssertArgumentException::AssertArgumentException(const char* condStr,
 174                                                  const char* argDesc,
 175                                                  const char* function,
 176                                                  const char* file,
 177                                                  unsigned line,
 178                                                  const char* fmt,
 179                                                  ...)
 180     : Exception()
 181 {
 182   va_list args;
 183   va_start(args, fmt);
 184   construct("Illegal argument detected",
 185             (std::string("`") + argDesc + "' is a bad argument; expected "
 186              + condStr + " to hold")
 187                 .c_str(),
 188             function,
 189             file,
 190             line,
 191             fmt,
 192             args);
 193   va_end(args);
 194 }
 195
 196 AssertArgumentException::AssertArgumentException(const char* condStr,
 197                                                  const char* argDesc,
 198                                                  const char* function,
 199                                                  const char* file,
 200                                                  unsigned line)
 201     : Exception()
 202 {
 203   construct("Illegal argument detected",
 204             (std::string("`") + argDesc + "' is a bad argument; expected "
 205              + condStr + " to hold")
 206                 .c_str(),
 207             function,
 208             file,
 209             line);
 210 }
 211
 212 }  // namespace CVC4