From 2e5cc613d280fab1be89d8360250cbc3a1635ac9 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 9 Jan 2018 22:05:02 -0800 Subject: Cleaning up throw specifiers on Exception and subclasses. (#1475) --- src/base/exception.h | 29 +++++++----- src/base/exception.i | 4 +- src/expr/datatype.h | 2 +- src/expr/expr_template.cpp | 30 ++++++------ src/expr/expr_template.h | 34 +++++-------- src/expr/node.cpp | 26 +++++----- src/expr/node.h | 21 ++++---- src/options/option_exception.h | 9 ++-- src/parser/parser_exception.h | 79 ++++++++++++------------------- src/smt/logic_exception.h | 2 +- src/theory/arith/delta_rational.cpp | 17 +++---- src/theory/arith/delta_rational.h | 8 ++-- src/theory/arith/theory_arith_private.cpp | 6 +-- src/theory/arith/theory_arith_private.h | 6 +-- src/theory/type_enumerator.h | 5 +- src/util/rational_cln_imp.cpp | 1 - src/util/rational_gmp_imp.h | 1 + 17 files changed, 132 insertions(+), 148 deletions(-) diff --git a/src/base/exception.h b/src/base/exception.h index 01a054b19..04b155571 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -32,24 +32,24 @@ namespace CVC4 { class CVC4_PUBLIC Exception : public std::exception { -protected: + protected: std::string d_msg; -public: + public: // Constructors - Exception() throw() : d_msg("Unknown exception") {} - Exception(const std::string& msg) throw() : d_msg(msg) {} - Exception(const char* msg) throw() : d_msg(msg) {} + Exception() : d_msg("Unknown exception") {} + Exception(const std::string& msg) : d_msg(msg) {} + Exception(const char* msg) : d_msg(msg) {} // Destructor - virtual ~Exception() throw() {} + virtual ~Exception() {} // NON-VIRTUAL METHOD for setting and printing the error message - void setMessage(const std::string& msg) throw() { d_msg = msg; } - std::string getMessage() const throw() { return d_msg; } + void setMessage(const std::string& msg) { d_msg = msg; } + std::string getMessage() const { return d_msg; } // overridden from base class std::exception - virtual const char* what() const throw() { return d_msg.c_str(); } + const char* what() const noexcept override { return d_msg.c_str(); } /** * Get this exception as a string. Note that @@ -63,7 +63,8 @@ public: * toString(), there is no stream, so the parameters are default * and you'll get exprs and types printed using the AST language. */ - std::string toString() const throw() { + std::string toString() const + { std::stringstream ss; toStream(ss); return ss.str(); @@ -74,7 +75,7 @@ public: * a derived class, it's recommended that this method print the * type of exception before the actual message. */ - virtual void toStream(std::ostream& os) const throw() { os << d_msg; } + virtual void toStream(std::ostream& os) const { os << d_msg; } };/* class Exception */ @@ -116,8 +117,10 @@ public: static std::string formatVariadic(const char* format, ...); };/* class IllegalArgumentException */ -inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { +inline std::ostream& operator<<(std::ostream& os, + const Exception& e) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const Exception& e) +{ e.toStream(os); return os; } diff --git a/src/base/exception.i b/src/base/exception.i index 083670567..429d13a63 100644 --- a/src/base/exception.i +++ b/src/base/exception.i @@ -2,8 +2,8 @@ #include "base/exception.h" %} -%ignore CVC4::operator<<(std::ostream&, const Exception&) throw(); -%ignore CVC4::Exception::Exception(const char*) throw(); +%ignore CVC4::operator<<(std::ostream&, const Exception&); +%ignore CVC4::Exception::Exception(const char*); %typemap(javabase) CVC4::Exception "java.lang.RuntimeException"; %rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 9e3ad07f8..fffabac77 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -88,7 +88,7 @@ public: * An exception that is thrown when a datatype resolution fails. */ class CVC4_PUBLIC DatatypeResolutionException : public Exception { -public: + public: inline DatatypeResolutionException(std::string msg); };/* class DatatypeResolutionException */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 6dbc2256c..0ed3601fc 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -54,31 +54,33 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { } } -TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() : - Exception(t.d_msg), d_expr(new Expr(t.getExpression())) { +TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) + : Exception(t.d_msg), d_expr(new Expr(t.getExpression())) +{ } -TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() : - Exception(message), d_expr(new Expr(expr)) { +TypeCheckingException::TypeCheckingException(const Expr& expr, + std::string message) + : Exception(message), d_expr(new Expr(expr)) +{ } -TypeCheckingException::TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) throw() : - Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) { +TypeCheckingException::TypeCheckingException( + ExprManager* em, const TypeCheckingExceptionPrivate* exc) + : Exception(exc->getMessage()), + d_expr(new Expr(em, new Node(exc->getNode()))) +{ } -TypeCheckingException::~TypeCheckingException() throw() { - delete d_expr; -} +TypeCheckingException::~TypeCheckingException() { delete d_expr; } -void TypeCheckingException::toStream(std::ostream& os) const throw() { +void TypeCheckingException::toStream(std::ostream& os) const +{ os << "Error during type checking: " << d_msg << endl << "The ill-typed expression: " << *d_expr; } -Expr TypeCheckingException::getExpression() const throw() { - return *d_expr; -} +Expr TypeCheckingException::getExpression() const { return *d_expr; } Expr::Expr() : d_node(new Node), diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index ead50c1ab..9656781a8 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -83,44 +83,40 @@ namespace expr { * Exception thrown in the case of type-checking errors. */ class CVC4_PUBLIC TypeCheckingException : public Exception { - + private: friend class SmtEngine; friend class smt::SmtEnginePrivate; -private: - /** The expression responsible for the error */ Expr* d_expr; -protected: - - TypeCheckingException() throw() : Exception() {} + protected: + TypeCheckingException() : Exception() {} TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) throw(); + const TypeCheckingExceptionPrivate* exc); -public: - - TypeCheckingException(const Expr& expr, std::string message) throw(); + public: + TypeCheckingException(const Expr& expr, std::string message); /** Copy constructor */ - TypeCheckingException(const TypeCheckingException& t) throw(); + TypeCheckingException(const TypeCheckingException& t); /** Destructor */ - ~TypeCheckingException() throw(); + ~TypeCheckingException() override; /** * Get the Expr that caused the type-checking to fail. * * @return the expr */ - Expr getExpression() const throw(); + Expr getExpression() const; /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const throw(); + void toStream(std::ostream& out) const override; friend class ExprManager; };/* class TypeCheckingException */ @@ -129,13 +125,9 @@ public: * Exception thrown in case of failure to export */ class CVC4_PUBLIC ExportUnsupportedException : public Exception { -public: - ExportUnsupportedException() throw(): - Exception("export unsupported") { - } - ExportUnsupportedException(const char* msg) throw(): - Exception(msg) { - } + public: + ExportUnsupportedException() : Exception("export unsupported") {} + ExportUnsupportedException(const char* msg) : Exception(msg) {} };/* class DatatypeExportUnsupportedException */ std::ostream& operator<<(std::ostream& out, diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 126feadd8..110925f41 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -27,9 +27,9 @@ using namespace std; namespace CVC4 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, - std::string message) throw() : - Exception(message), - d_node(new Node(node)) { + std::string message) + : Exception(message), d_node(new Node(node)) +{ #ifdef CVC4_DEBUG LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); if(current != NULL){ @@ -38,21 +38,25 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, #endif /* CVC4_DEBUG */ } -TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { - delete d_node; -} +TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; } -void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { +void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const +{ os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node; } -NodeTemplate TypeCheckingExceptionPrivate::getNode() const throw() { +NodeTemplate TypeCheckingExceptionPrivate::getNode() const +{ return *d_node; } -UnknownTypeException::UnknownTypeException(TNode n) throw() : - TypeCheckingExceptionPrivate(n, "this expression contains an element of unknown type (such as an abstract value);" - " its type cannot be computed until it is substituted away") { +UnknownTypeException::UnknownTypeException(TNode n) + : TypeCheckingExceptionPrivate( + n, + "this expression contains an element of unknown type (such as an " + "abstract value);" + " its type cannot be computed until it is substituted away") +{ } /** Is this node constant? (and has that been computed yet?) */ diff --git a/src/expr/node.h b/src/expr/node.h index 66f8b0a47..fd3d20afa 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -66,44 +66,39 @@ class NodeTemplate; * thrown by node.getType(). */ class TypeCheckingExceptionPrivate : public Exception { - -private: - + private: /** The node responsible for the failure */ NodeTemplate* d_node; -public: - + public: /** * Construct the exception with the problematic node and the message * @param node the problematic node * @param message the message explaining the failure */ - TypeCheckingExceptionPrivate(NodeTemplate node, std::string message) throw(); + TypeCheckingExceptionPrivate(NodeTemplate node, std::string message); /** Destructor */ - ~TypeCheckingExceptionPrivate() throw (); + ~TypeCheckingExceptionPrivate() override; /** * Get the Node that caused the type-checking to fail. * @return the node */ - NodeTemplate getNode() const throw(); + NodeTemplate getNode() const; /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const throw(); + void toStream(std::ostream& out) const override; };/* class TypeCheckingExceptionPrivate */ class UnknownTypeException : public TypeCheckingExceptionPrivate { -public: - - UnknownTypeException(NodeTemplate node) throw(); - + public: + UnknownTypeException(NodeTemplate node); };/* class UnknownTypeException */ /** diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 4cea29592..12c69193e 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -30,9 +30,10 @@ namespace CVC4 { * class, below) should be used instead. */ class CVC4_PUBLIC OptionException : public CVC4::Exception { -public: - OptionException(const std::string& s) throw() : - CVC4::Exception("Error in option parsing: " + s) { + public: + OptionException(const std::string& s) + : CVC4::Exception("Error in option parsing: " + s) + { } };/* class OptionException */ @@ -41,7 +42,7 @@ public: * unrecognized or unsupported option key. */ class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException { -public: + public: UnrecognizedOptionException() : CVC4::OptionException("Unrecognized informational or option key or setting") { } diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 48eb43e33..5e1be70e8 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -29,40 +29,33 @@ namespace CVC4 { namespace parser { class CVC4_PUBLIC ParserException : public Exception { -public: + public: // Constructors - ParserException() throw() : - d_filename(), - d_line(0), - d_column(0) { - } + ParserException() : d_filename(), d_line(0), d_column(0) {} - ParserException(const std::string& msg) throw() : - Exception(msg), - d_filename(), - d_line(0), - d_column(0) { + ParserException(const std::string& msg) + : Exception(msg), d_filename(), d_line(0), d_column(0) + { } - ParserException(const char* msg) throw() : - Exception(msg), - d_filename(), - d_line(0), - d_column(0) { + ParserException(const char* msg) + : Exception(msg), d_filename(), d_line(0), d_column(0) + { } - ParserException(const std::string& msg, const std::string& filename, - unsigned long line, unsigned long column) throw() : - Exception(msg), - d_filename(filename), - d_line(line), - d_column(column) { + ParserException(const std::string& msg, + const std::string& filename, + unsigned long line, + unsigned long column) + : Exception(msg), d_filename(filename), d_line(line), d_column(column) + { } // Destructor - virtual ~ParserException() throw() {} + ~ParserException() override {} - virtual void toStream(std::ostream& os) const throw() { + void toStream(std::ostream& os) const override + { if( d_line > 0 ) { os << "Parse Error: " << d_filename << ":" << d_line << "." << d_column << ": " << d_msg; @@ -71,44 +64,34 @@ public: } } - std::string getFilename() const throw() { - return d_filename; - } + std::string getFilename() const { return d_filename; } - int getLine() const throw() { - return d_line; - } + int getLine() const { return d_line; } - int getColumn() const throw() { - return d_column; - } + int getColumn() const { return d_column; } -protected: + protected: std::string d_filename; unsigned long d_line; unsigned long d_column; };/* class ParserException */ class CVC4_PUBLIC ParserEndOfFileException : public ParserException { -public: - + public: // Constructors same as ParserException's - ParserEndOfFileException() throw() : - ParserException() { - } + ParserEndOfFileException() : ParserException() {} - ParserEndOfFileException(const std::string& msg) throw() : - ParserException(msg) { - } + ParserEndOfFileException(const std::string& msg) : ParserException(msg) {} - ParserEndOfFileException(const char* msg) throw() : - ParserException(msg) { - } + ParserEndOfFileException(const char* msg) : ParserException(msg) {} - ParserEndOfFileException(const std::string& msg, const std::string& filename, - unsigned long line, unsigned long column) throw() : - ParserException(msg, filename, line, column) { + ParserEndOfFileException(const std::string& msg, + const std::string& filename, + unsigned long line, + unsigned long column) + : ParserException(msg, filename, line, column) + { } };/* class ParserEndOfFileException */ diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index 5d5b02162..86e386e9a 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -27,7 +27,7 @@ namespace CVC4 { class CVC4_PUBLIC LogicException : public CVC4::Exception { -public: + public: LogicException() : Exception("Feature used while operating in " "incorrect state") { diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 467f868a3..fba7fdaf6 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -72,16 +72,17 @@ void DeltaRational::seperatingDelta(Rational& res, const DeltaRational& a, const } } - -DeltaRationalException::DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (){ - std::stringstream ss; - ss << "Operation [" << op << "] between DeltaRational values "; - ss << a << " and " << b << " is not a DeltaRational."; - setMessage(ss.str()); +DeltaRationalException::DeltaRationalException(const char* op, + const DeltaRational& a, + const DeltaRational& b) +{ + std::stringstream ss; + ss << "Operation [" << op << "] between DeltaRational values "; + ss << a << " and " << b << " is not a DeltaRational."; + setMessage(ss.str()); } -DeltaRationalException::~DeltaRationalException() throw () { } - +DeltaRationalException::~DeltaRationalException() {} Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){ if(isIntegral() && y.isIntegral()){ diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index b0ea8a9c1..7a1c18ea2 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -31,9 +31,11 @@ namespace CVC4 { class DeltaRational; class DeltaRationalException : public Exception { -public: - DeltaRationalException(const char* op, const DeltaRational& a, const DeltaRational& b) throw (); - virtual ~DeltaRationalException() throw (); + public: + DeltaRationalException(const char* op, + const DeltaRational& a, + const DeltaRational& b); + ~DeltaRationalException() override; }; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index f281bdfcc..f05f47595 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -311,13 +311,13 @@ void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_congruenceManager.setMasterEqualityEngine(eq); } -TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) throw (){ +TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) +{ stringstream ss; ss << "Cannot construct a model for " << n << " as " << endl << msg; setMessage(ss.str()); } -TheoryArithPrivate::ModelException::~ModelException() throw (){ } - +TheoryArithPrivate::ModelException::~ModelException() {} TheoryArithPrivate::Statistics::Statistics() : d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0) diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index ff60e8436..912bae5e6 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -396,9 +396,9 @@ private: bool replayLog(ApproximateSimplex* approx); class ModelException : public Exception { - public: - ModelException(TNode n, const char* msg) throw (); - virtual ~ModelException() throw (); + public: + ModelException(TNode n, const char* msg); + ~ModelException() override; }; /** diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 18ed6d661..f90a06833 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -29,8 +29,9 @@ namespace theory { class NoMoreValuesException : public Exception { public: - NoMoreValuesException(TypeNode n) throw() : - Exception("No more values for type `" + n.toString() + "'") { + NoMoreValuesException(TypeNode n) + : Exception("No more values for type `" + n.toString() + "'") + { } };/* class NoMoreValuesException */ diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 6250cbccd..aa893517b 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -98,7 +98,6 @@ Maybe Rational::fromDouble(double d) }catch(cln::floating_point_overflow_exception& fpoe){ return Maybe(); } - Unreachable(); } } /* namespace CVC4 */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 7c17ead15..153b237d7 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -84,6 +84,7 @@ public: /** * Constructs a Rational from a C string in a given base (defaults to 10). + * * Throws std::invalid_argument if the string is not a valid rational. * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). -- cgit v1.2.3