From 19847e87a8894d61b59d27bedd35aa73e44c126f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 20 Feb 2013 18:09:59 -0500 Subject: [PATCH] Some exception specification fixes in SmtEngine/Command infrastructure --- src/expr/command.cpp | 8 ++++++-- src/smt/smt_engine.cpp | 2 +- src/smt/smt_engine.h | 2 +- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index fa2a8d1f2..9edc77e39 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -703,8 +703,12 @@ Expr SimplifyCommand::getTerm() const throw() { } void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { - d_result = smtEngine->simplify(d_term); - d_commandStatus = CommandSuccess::instance(); + try { + d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } Expr SimplifyCommand::getResult() const throw() { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6b0d953dd..e7c0999da 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3039,7 +3039,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L return n.toExpr(); } -Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { +Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index cdae68d96..fecfba14a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -444,7 +444,7 @@ public: * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) throw(ModalException, LogicException); + Expr getValue(const Expr& e) throw(ModalException, TypeCheckingException, LogicException); /** * Add a function to the set of expressions whose value is to be -- 2.30.2