From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 10 Mar 2011 21:05:13 +0000 (+0000)
Subject: Fix bug 246 (occasional buffer overflow related to varargs in assertion-failure strin... 
X-Git-Tag: cvc5-1.0.0~8662
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f4764b2f0e64be5df31cd87a27363cf59045665;p=cvc5.git

Fix bug 246 (occasional buffer overflow related to varargs in assertion-failure string construction) and addition of an assert_white unit test check for the issue
---

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 84f970e87..ea0b26248 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -54,7 +54,7 @@ void AssertionException::construct(const char* header, const char* extra,
     if(size < n) {
       va_list args_copy;
       va_copy(args_copy, args);
-      size += vsnprintf(buf + size, n - size, fmt, args);
+      size += vsnprintf(buf + size, n - size, fmt, args_copy);
       va_end(args_copy);
 
       if(size < n) {
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 389f2aa1b..75006ed12 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -71,6 +71,31 @@ public:
     } catch(...) {
       TS_FAIL("Threw the wrong kind of exception !");
     }
+
+    // Now test an assert with a format that drives it over the 512
+    // byte initial buffer.  This was a bug in r1441, see bug 246:
+    // http://goedel.cims.nyu.edu/bugzilla3/show_bug.cgi?id=246
+    string fmt = string(200, 'x') + " %s " + string(200, 'x');
+    string arg(200, 'y');
+    try {
+      AlwaysAssert(false, fmt.c_str(), arg.c_str());
+      TS_FAIL("Should have thrown an exception !");
+    } catch(AssertionException& e) {
+      // we don't want to match on the entire string, because it may
+      // have an absolute path to the unit test binary, line number
+      // info, etc.
+      const char* theString = e.toString().c_str();
+      const char* firstPart =
+        "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n";
+      string lastPartStr = "\n\n  false\n" + string(200, 'x') + " " +
+        string(200, 'y') + " " + string(200, 'x');
+      const char* lastPart = lastPartStr.c_str();
+      TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0);
+      TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart),
+                        lastPart, strlen(lastPart)) == 0);
+    } catch(...) {
+      TS_FAIL("Threw the wrong kind of exception !");
+    }
   }
 
   void testUnreachable() {