mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 02:42:02 +00:00
Merge pull request #1894 from waywardmonkeys/cleanup-warning-generation
Cleanup warning generation
This commit is contained in:
commit
695a9a69d1
2 changed files with 15 additions and 78 deletions
|
@ -25,7 +25,6 @@ Revision History:
|
||||||
#include "util/vector.h"
|
#include "util/vector.h"
|
||||||
|
|
||||||
#ifdef _WINDOWS
|
#ifdef _WINDOWS
|
||||||
#define PRF sprintf_s
|
|
||||||
#define VPRF vsprintf_s
|
#define VPRF vsprintf_s
|
||||||
|
|
||||||
void STD_CALL myInvalidParameterHandler(
|
void STD_CALL myInvalidParameterHandler(
|
||||||
|
@ -54,7 +53,6 @@ void STD_CALL myInvalidParameterHandler(
|
||||||
|
|
||||||
|
|
||||||
#else
|
#else
|
||||||
#define PRF snprintf
|
|
||||||
#define VPRF vsnprintf
|
#define VPRF vsnprintf
|
||||||
#define BEGIN_ERR_HANDLER() {}
|
#define BEGIN_ERR_HANDLER() {}
|
||||||
#define END_ERR_HANDLER() {}
|
#define END_ERR_HANDLER() {}
|
||||||
|
@ -64,7 +62,6 @@ static bool g_warning_msgs = true;
|
||||||
static bool g_use_std_stdout = false;
|
static bool g_use_std_stdout = false;
|
||||||
static std::ostream* g_error_stream = nullptr;
|
static std::ostream* g_error_stream = nullptr;
|
||||||
static std::ostream* g_warning_stream = nullptr;
|
static std::ostream* g_warning_stream = nullptr;
|
||||||
static bool g_show_error_msg_prefix = true;
|
|
||||||
|
|
||||||
void send_warnings_to_stdout(bool flag) {
|
void send_warnings_to_stdout(bool flag) {
|
||||||
g_use_std_stdout = flag;
|
g_use_std_stdout = flag;
|
||||||
|
@ -82,61 +79,24 @@ void set_warning_stream(std::ostream* strm) {
|
||||||
g_warning_stream = strm;
|
g_warning_stream = strm;
|
||||||
}
|
}
|
||||||
|
|
||||||
void disable_error_msg_prefix() {
|
|
||||||
g_show_error_msg_prefix = false;
|
|
||||||
}
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
// [Leo]: Do we need this?
|
|
||||||
static void string2ostream(std::ostream& out, char const* msg) {
|
|
||||||
svector<char> buff;
|
|
||||||
buff.resize(10);
|
|
||||||
BEGIN_ERR_HANDLER();
|
|
||||||
while (true) {
|
|
||||||
int nc = PRF(buff.c_ptr(), buff.size(), msg);
|
|
||||||
if (nc >= 0 && nc < static_cast<int>(buff.size()))
|
|
||||||
break; // success
|
|
||||||
buff.resize(buff.size()*2 + 1);
|
|
||||||
}
|
|
||||||
END_ERR_HANDLER();
|
|
||||||
out << buff.c_ptr();
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
void format2ostream(std::ostream & out, char const* msg, va_list args) {
|
void format2ostream(std::ostream & out, char const* msg, va_list args) {
|
||||||
svector<char> buff;
|
svector<char> buff;
|
||||||
#if !defined(_WINDOWS) && defined(_AMD64_)
|
|
||||||
// see comment below.
|
|
||||||
buff.resize(1024);
|
|
||||||
#else
|
|
||||||
buff.resize(128);
|
|
||||||
#endif
|
|
||||||
BEGIN_ERR_HANDLER();
|
BEGIN_ERR_HANDLER();
|
||||||
while (true) {
|
|
||||||
int nc = VPRF(buff.c_ptr(), buff.size(), msg, args);
|
va_list args_copy;
|
||||||
#if !defined(_WINDOWS) && defined(_AMD64_)
|
va_copy(args_copy, args);
|
||||||
// For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
|
#ifdef _WINDOWS
|
||||||
// Z3 crashes when trying to use va_list args again.
|
size_t msg_len = _vscprintf(msg, args_copy);
|
||||||
// Hack: I truncate the message instead of expanding the buffer to make sure that
|
|
||||||
// va_list args is only used once.
|
|
||||||
END_ERR_HANDLER();
|
|
||||||
if (nc < 0) {
|
|
||||||
// vsnprintf didn't work, so we just print the msg
|
|
||||||
out << msg;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
if (nc >= static_cast<int>(buff.size())) {
|
|
||||||
// truncate the message
|
|
||||||
buff[buff.size() - 1] = 0;
|
|
||||||
}
|
|
||||||
out << buff.c_ptr();
|
|
||||||
return;
|
|
||||||
#else
|
#else
|
||||||
if (nc >= 0 && nc < static_cast<int>(buff.size()))
|
size_t msg_len = vsnprintf(NULL, 0, msg, args_copy);
|
||||||
break; // success
|
|
||||||
buff.resize(buff.size()*2 + 1);
|
|
||||||
#endif
|
#endif
|
||||||
}
|
va_end(args_copy);
|
||||||
|
|
||||||
|
// +1 is for NUL termination.
|
||||||
|
buff.resize(msg_len + 1);
|
||||||
|
|
||||||
|
VPRF(buff.c_ptr(), buff.size(), msg, args);
|
||||||
|
|
||||||
END_ERR_HANDLER();
|
END_ERR_HANDLER();
|
||||||
out << buff.c_ptr();
|
out << buff.c_ptr();
|
||||||
}
|
}
|
||||||
|
|
|
@ -31,30 +31,7 @@ void set_warning_stream(std::ostream* strm);
|
||||||
|
|
||||||
void warning_msg(const char * msg, ...);
|
void warning_msg(const char * msg, ...);
|
||||||
|
|
||||||
void disable_error_msg_prefix();
|
|
||||||
|
|
||||||
void format2ostream(std::ostream& out, char const* fmt, va_list args);
|
void format2ostream(std::ostream& out, char const* fmt, va_list args);
|
||||||
|
|
||||||
class warning_displayer {
|
|
||||||
const char * m_msg;
|
|
||||||
bool m_displayed;
|
|
||||||
public:
|
|
||||||
warning_displayer(const char * msg):
|
|
||||||
m_msg(msg),
|
|
||||||
m_displayed(false) {
|
|
||||||
}
|
|
||||||
|
|
||||||
void sign() {
|
|
||||||
if (!m_displayed) {
|
|
||||||
warning_msg(m_msg);
|
|
||||||
m_displayed = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void reset() {
|
|
||||||
m_displayed = false;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif /* WARNING_H_ */
|
#endif /* WARNING_H_ */
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue