GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/base/check.cpp Lines: 48 71 67.6 %
Date: 2021-03-22 Branches: 29 66 43.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Morgan Deters, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
2
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
2
  int n = 512;
55
  char* buf;
56
2
  buf = new char[n];
57
58
  for (;;)
59
  {
60
    int size;
61
2
    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
2
      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
2
    if (size < n)
78
    {
79
      va_list args_copy;
80
2
      va_copy(args_copy, args);
81
2
      size += vsnprintf(buf + size, n - size, fmt, args_copy);
82
2
      va_end(args_copy);
83
84
2
      if (size < n)
85
      {
86
2
        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
4
  setMessage(std::string(buf));
100
101
#ifdef CVC4_DEBUG
102
2
  LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
103
2
  if (buffer != NULL)
104
  {
105
    if (buffer->getContents() == NULL)
106
    {
107
      buffer->setContents(buf);
108
    }
109
  }
110
#endif /* CVC4_DEBUG */
111
2
  delete[] buf;
112
2
}
113
114
12
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
12
  int n = 256;
123
  char* buf;
124
125
  for (;;)
126
  {
127
18
    buf = new char[n];
128
129
    int size;
130
18
    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
18
      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
18
    if (size < n)
147
    {
148
12
      break;
149
    }
150
    else
151
    {
152
      // try again with a buffer that's large enough
153
6
      n = size + 1;
154
6
      delete[] buf;
155
    }
156
6
  }
157
158
12
  setMessage(std::string(buf));
159
160
#ifdef CVC4_DEBUG
161
12
  LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
162
12
  if (buffer != NULL)
163
  {
164
    if (buffer->getContents() == NULL)
165
    {
166
      buffer->setContents(buf);
167
    }
168
  }
169
#endif /* CVC4_DEBUG */
170
12
  delete[] buf;
171
12
}
172
173
2
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
2
                                                 ...)
180
2
    : Exception()
181
{
182
  va_list args;
183
2
  va_start(args, fmt);
184
2
  construct("Illegal argument detected",
185
4
            (std::string("`") + argDesc + "' is a bad argument; expected "
186
4
             + condStr + " to hold")
187
                .c_str(),
188
            function,
189
            file,
190
            line,
191
            fmt,
192
            args);
193
2
  va_end(args);
194
2
}
195
196
12
AssertArgumentException::AssertArgumentException(const char* condStr,
197
                                                 const char* argDesc,
198
                                                 const char* function,
199
                                                 const char* file,
200
12
                                                 unsigned line)
201
12
    : Exception()
202
{
203
12
  construct("Illegal argument detected",
204
24
            (std::string("`") + argDesc + "' is a bad argument; expected "
205
24
             + condStr + " to hold")
206
                .c_str(),
207
            function,
208
            file,
209
            line);
210
12
}
211
212
26676
}  // namespace CVC4