From 5907f687f0a3d5b983884431c43c509dcd725d82 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 3 May 2018 14:27:39 +0100
Subject: [PATCH 1/2] fix potential non-zero termination of a string buffer

---
 src/util/tempdir.cpp | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp
index 7a2f9a460a2..0eae3389581 100644
--- a/src/util/tempdir.cpp
+++ b/src/util/tempdir.cpp
@@ -15,7 +15,7 @@ Author: CM Wintersteiger
 #endif
 
 #include <cstdlib>
-#include <cstring>
+#include <vector>
 
 #if defined(__linux__) || \
     defined(__FreeBSD_kernel__) || \
@@ -34,17 +34,18 @@ std::string get_temporary_directory(const std::string &name_template)
   std::string result;
 
   #ifdef _WIN32
-    DWORD dwBufSize = MAX_PATH;
-    char lpPathBuffer[MAX_PATH];
+    DWORD dwBufSize = MAX_PATH+1;
+    char lpPathBuffer[MAX_PATH+1];
     DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer);
 
     if(dwRetVal > dwBufSize || (dwRetVal == 0))
       throw "GetTempPath failed"; // NOLINT(readability/throw)
 
-    char t[MAX_PATH];
-
-    strncpy(t, name_template.c_str(), MAX_PATH);
+    // GetTempFileNameA produces <path>\<pre><uuuu>.TMP
+    // where <pre> = "TLO"
+    // Thus, we must make the buffer 1+3+4+1+3=12 characters longer.
 
+    char t[MAX_PATH];
     UINT uRetVal=GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
     if(uRetVal == 0)
       throw "GetTempFileName failed"; // NOLINT(readability/throw)
@@ -64,9 +65,9 @@ std::string get_temporary_directory(const std::string &name_template)
       prefixed_name_template+='/';
     prefixed_name_template+=name_template;
 
-    char t[1000];
-    strncpy(t, prefixed_name_template.c_str(), 1000);
-    const char *td = mkdtemp(t);
+    std::vector<char> t(prefixed_name_template.begin(), prefixed_name_template.end());
+    t.push_back('\0'); // add the zero
+    const char *td = mkdtemp(t.data());
     if(!td)
       throw "mkdtemp failed";
     result=std::string(td);

From 9609a52fe49013f246f375a97b0d92e08b373675 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 3 May 2018 21:51:38 +0100
Subject: [PATCH 2/2] simplify use of get_temporary_directory

---
 src/goto-cc/compile.cpp | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 98550ce7375..fd92c7aeb63 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -226,12 +226,6 @@ bool compilet::add_files_from_archive(
   const std::string &file_name,
   bool thin_archive)
 {
-#ifdef _WIN32
-  char td[MAX_PATH + 1];
-#else
-  char td[] = "goto-cc.XXXXXX";
-#endif
-
   std::stringstream cmd;
   FILE *stream;
 
@@ -239,7 +233,7 @@ bool compilet::add_files_from_archive(
 
   if(!thin_archive)
   {
-    tstr = get_temporary_directory(td);
+    tstr = get_temporary_directory("goto-cc.XXXXXX");
 
     if(tstr=="")
     {