diff options
author | Tim King <taking@google.com> | 2015-11-13 09:53:19 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-11-23 16:44:20 -0800 |
commit | 8098d95adcbb65d2d76322316f5a10c996f0eb8d (patch) | |
tree | fde36a569539d3abb9c5581ea80b90311669aa93 /src | |
parent | 9c27a43de4120f9c571757b8541884013a37fa3d (diff) |
Freeing memory allocated for signal handling.
Diffstat (limited to 'src')
-rw-r--r-- | src/main/driver_unified.cpp | 2 | ||||
-rw-r--r-- | src/main/main.h | 4 | ||||
-rw-r--r-- | src/main/util.cpp | 8 |
3 files changed, 13 insertions, 1 deletions
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 */ |