mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Improve format2ostream.
Instead of looping to find a big enough buffer, we can call the correct function to calculate it, remembering to add an extra character for NUL termination. We also correctly do a va_copy of the args to avoid crashes on some platforms.
This commit is contained in:
parent
21cf218a9f
commit
129353542c
|
@ -16,8 +16,8 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<stdio.h>
|
||||
#include<stdarg.h>
|
||||
#include <stdio.h>
|
||||
#include <stdarg.h>
|
||||
|
||||
#include "util/error_codes.h"
|
||||
#include "util/util.h"
|
||||
|
@ -86,38 +86,22 @@ void disable_error_msg_prefix() {
|
|||
|
||||
void format2ostream(std::ostream & out, char const* msg, va_list args) {
|
||||
svector<char> buff;
|
||||
#if !defined(_WINDOWS) && defined(_AMD64_)
|
||||
// see comment below.
|
||||
buff.resize(1024);
|
||||
#else
|
||||
buff.resize(128);
|
||||
#endif
|
||||
BEGIN_ERR_HANDLER();
|
||||
while (true) {
|
||||
int nc = VPRF(buff.c_ptr(), buff.size(), msg, args);
|
||||
#if !defined(_WINDOWS) && defined(_AMD64_)
|
||||
// For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
|
||||
// Z3 crashes when trying to use va_list args again.
|
||||
// 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;
|
||||
|
||||
va_list args_copy;
|
||||
va_copy(args_copy, args);
|
||||
#ifdef _WINDOWS
|
||||
size_t msg_len = _vscprintf(msg, args_copy);
|
||||
#else
|
||||
if (nc >= 0 && nc < static_cast<int>(buff.size()))
|
||||
break; // success
|
||||
buff.resize(buff.size()*2 + 1);
|
||||
size_t msg_len = vsnprintf(NULL, 0, msg, args_copy);
|
||||
#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();
|
||||
out << buff.c_ptr();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue