1 files changed, 58 insertions, 19 deletions

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index d8eee50bc..87bdfcfa5 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "base/exception.h"
+
 #include <string>
 #include <cstdio>
 #include <cstdlib>
@@ -24,12 +25,58 @@
 
 using namespace std;
 
-#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument."
-
 namespace CVC4 {
+
+char* IllegalArgumentException::s_header = "Illegal argument detected";
+
+std::string IllegalArgumentException::formatVariadic() {
+  return std::string();
+}
+
+std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
+  va_list args;
+  va_start(args, format);
+
+  int n = 512;
+  char* buf = NULL;
+
+  for (int i = 0; i < 2; ++i){
+    Assert(n > 0);
+    if(buf != NULL){
+      delete [] buf;
+    }
+    buf = new char[n];
+
+    va_list args_copy;
+    va_copy(args_copy, args);
+    int size = vsnprintf(buf, n, format, args);
+    va_end(args_copy);
+
+    if(size >= n){
+      buf[n-1] = '\0';
+      n = size + 1;
+    } else {
+      break;
+    }
+  }
+  // buf is not NULL is an invariant.
+  // buf is also 0 terminated.
+  Assert(buf != NULL);
+  std::string result(buf);
+  delete [] buf;
+  va_end(args);
+  return result;
+}
+
+std::string IllegalArgumentException::format_extra(const char* condStr, const char* argDesc){
+  return ( std::string("`") + argDesc + "' is a bad argument"
+           + (*condStr == '\0' ? std::string() :
+              ( std::string("; expected ") +
+                condStr + " to hold" )) );
+}
+
 void IllegalArgumentException::construct(const char* header, const char* extra,
-                                         const char* function, const char* fmt,
-                                         va_list args) {
+                                         const char* function, const char* tail) {
   // try building the exception msg with a smallish buffer first,
   // then with a larger one if sprintf tells us to.
   int n = 512;
@@ -40,25 +87,17 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
     int size;
     if(extra == NULL) {
-      size = snprintf(buf, n, "%s\n%s\n",
-                      header, function);
+      size = snprintf(buf, n, "%s\n%s\n%s",
+                      header, function, tail);
     } else {
-      size = snprintf(buf, n, "%s\n%s\n\n  %s\n",
-                      header, function, extra);
+      size = snprintf(buf, n, "%s\n%s\n\n  %s\n%s",
+                      header, function, extra, tail);
     }
 
     if(size < n) {
-      va_list args_copy;
-      va_copy(args_copy, args);
-      size += vsnprintf(buf + size, n - size, fmt, args_copy);
-      va_end(args_copy);
-
-      if(size < n) {
-        break;
-      }
-    }
-
-    if(size >= n) {
+      break;
+    } else {
+      // size >= n
       // try again with a buffer that's large enough
       n = size + 1;
       delete [] buf;