From 129353542cde46e4591827c858f5a3ff144c8768 Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Sun, 21 Oct 2018 19:28:31 +0700
Subject: [PATCH] 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.
---
 src/util/warning.cpp | 46 +++++++++++++++-----------------------------
 1 file changed, 15 insertions(+), 31 deletions(-)

diff --git a/src/util/warning.cpp b/src/util/warning.cpp
index a2ebade85..d4de28782 100644
--- a/src/util/warning.cpp
+++ b/src/util/warning.cpp
@@ -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();
 }