From: Tim King <taking@google.com>
Date: Fri, 13 Nov 2015 17:53:19 +0000 (-0800)
Subject: Freeing memory allocated for signal handling.
X-Git-Tag: cvc5-1.0.0~6165
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8098d95adcbb65d2d76322316f5a10c996f0eb8d;p=cvc5.git

Freeing memory allocated for signal handling.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 7bc711910..c29ba55a4 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -609,5 +609,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   pTotalTime = NULL;
   pExecutor = NULL;
 
+  cvc4_shutdown();
+
   return returnValue;
 }
diff --git a/src/main/main.h b/src/main/main.h
index 01f337ef4..a2e813c6c 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -59,6 +59,10 @@ extern CVC4_THREADLOCAL(Options*) pOptions;
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw(Exception);
 
+/** Shutdown the driver. Frees memory for the signal handlers. */
+void cvc4_shutdown() throw();
+
+
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 3b7c6b95a..927802496 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -249,7 +249,7 @@ void cvc4_init() throw(Exception) {
     }
   }
   cvc4StackSize = limit.rlim_cur;
-  cvc4StackBase = &ss;
+  cvc4StackBase = ss.ss_sp;
 
   struct sigaction act1;
   act1.sa_sigaction = sigint_handler;
@@ -289,5 +289,11 @@ void cvc4_init() throw(Exception) {
   default_terminator = set_terminate(cvc4terminate);
 }
 
+void cvc4_shutdown() throw () {
+  free(cvc4StackBase);
+  cvc4StackBase = NULL;
+  cvc4StackSize = 0;
+}
+
 }/* CVC4::main namespace */
 }/* CVC4 namespace */