1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
/********************* */
/** Assert.cpp
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Assertion utility classes, functions, and exceptions. Implementation.
**/
#include <new>
#include <cstdarg>
#include <cstdio>
#include "util/Assert.h"
#include "util/exception.h"
#include "cvc4_config.h"
#include "config.h"
using namespace std;
namespace CVC4 {
#ifdef CVC4_DEBUG
__thread CVC4_PUBLIC const char* s_debugAssertionFailure = NULL;
#endif /* CVC4_DEBUG */
void AssertionException::construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt,
va_list args) {
// try building the exception msg with a smallish buffer first,
// then with a larger one if sprintf tells us to.
int n = 512;
char* buf;
for(;;) {
buf = new char[n];
int size;
if(extra == NULL) {
size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
header, function, file, line);
} else {
size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n",
header, function, file, line, extra);
}
if(size < n) {
va_list args_copy;
va_copy(args_copy, args);
size += vsnprintf(buf + size, n - size, fmt, args);
va_end(args_copy);
if(size < n) {
break;
}
}
if(size >= n) {
// try again with a buffer that's large enough
n = size + 1;
delete [] buf;
}
}
setMessage(string(buf));
#ifdef CVC4_DEBUG
// we leak buf[] but only in debug mode with assertions failing
s_debugAssertionFailure = buf;
#else /* CVC4_DEBUG */
delete [] buf;
#endif /* CVC4_DEBUG */
}
void AssertionException::construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line) {
// try building the exception msg with a smallish buffer first,
// then with a larger one if sprintf tells us to.
int n = 256;
char* buf;
for(;;) {
buf = new char[n];
int size;
if(extra == NULL) {
size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
header, function, file, line);
} else {
size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n",
header, function, file, line, extra);
}
if(size < n) {
break;
} else {
// try again with a buffer that's large enough
n = size + 1;
delete [] buf;
}
}
setMessage(string(buf));
#ifdef CVC4_DEBUG
// we leak buf[] but only in debug mode with assertions failing
s_debugAssertionFailure = buf;
#else /* CVC4_DEBUG */
delete [] buf;
#endif /* CVC4_DEBUG */
}
}/* CVC4 namespace */
|
