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/main/util.cpp | |
parent | 9c27a43de4120f9c571757b8541884013a37fa3d (diff) |
Freeing memory allocated for signal handling.
Diffstat (limited to 'src/main/util.cpp')
-rw-r--r-- | src/main/util.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
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 */ |