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