diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-08 22:04:02 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-08 22:04:02 -0800 |
commit | 3c6398194b01372720964590b2b07d93590e511d (patch) | |
tree | 1e1f40d79eeabe8b30524fe96d279a4f3d5b8fd7 /src/main | |
parent | 707e27e61addafdbcce5e7b6d32a61985f563dfb (diff) |
Removing more miscellaneous throw specifiers. (#1488)
Removing more miscellaneous throw specifiers.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/interactive_shell.cpp | 3 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 2 | ||||
-rw-r--r-- | src/main/util.cpp | 3 |
3 files changed, 5 insertions, 3 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 325f44769..4761ba07e 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -176,7 +176,8 @@ InteractiveShell::~InteractiveShell() { delete d_parser; } -Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) { +Command* InteractiveShell::readCommand() +{ char* lineBuf = NULL; string line = ""; diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index a3834a1e3..049b0649e 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -57,7 +57,7 @@ public: * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. */ - Command* readCommand() throw (UnsafeInterruptException); + Command* readCommand(); /** * Return the internal parser being used. diff --git a/src/main/util.cpp b/src/main/util.cpp index de6b47aa5..7086ea26f 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -345,7 +345,8 @@ void cvc4_init() default_terminator = set_terminate(cvc4terminate); } -void cvc4_shutdown() throw () { +void cvc4_shutdown() noexcept +{ #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK free(cvc4StackBase); |