From: Tim King Date: Sat, 6 Jan 2018 23:27:11 +0000 (-0800) Subject: Removing throw specifiers from src/parser/. (#1486) X-Git-Tag: cvc5-1.0.0~5378 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8497910df4d1c254b26f09c3dc5ee6191c970b12;p=cvc5.git Removing throw specifiers from src/parser/. (#1486) --- diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 915174982..a4bab5a8d 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -141,7 +141,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) - throw (InputStreamException) { +{ #ifdef _WIN32 if(useMmap) { useMmap = false; @@ -164,8 +164,7 @@ AntlrInputStream* AntlrInputStream::newStreamInputStream(std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException) { - +{ pANTLR3_INPUT_STREAM inputStream = NULL; pANTLR3_UINT8 inputStringCopy = NULL; LineBuffer* line_buffer = NULL; @@ -223,8 +222,7 @@ AntlrInputStream::newStreamInputStream(std::istream& input, AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) - throw (InputStreamException) { - +{ size_t input_size = input.size(); assert(input_size <= std::numeric_limits::max()); @@ -510,8 +508,7 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons } void AntlrInput::parseError(const std::string& message, bool eofException) - throw (ParserException) { - +{ string updatedMessage = parseErrorHelper((const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream), d_lexer->getCharPositionInLine(d_lexer), message); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index afede6bbf..d2bb8667d 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -88,14 +88,12 @@ public: * input will use the standard ANTLR3 I/O implementation. */ static AntlrInputStream* newFileInputStream(const std::string& name, - bool useMmap = false) - throw (InputStreamException); + bool useMmap = false); /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, const std::string& name, - bool lineBuffered = false) - throw (InputStreamException); + bool lineBuffered = false); /** Create a string input. * NOTE: the new AntlrInputStream will take ownership of input over @@ -105,8 +103,7 @@ public: * @param name the "filename" to use when reporting errors */ static AntlrInputStream* newStringInputStream(const std::string& input, - const std::string& name) - throw (InputStreamException); + const std::string& name); };/* class AntlrInputStream */ class Parser; @@ -223,13 +220,12 @@ protected: /** * Issue a non-fatal warning to the user with file, line, and column info. */ - void warning(const std::string& msg); + void warning(const std::string& msg) override; /** * Throws a ParserException with the given message. */ - void parseError(const std::string& msg, bool eofException = false) - throw (ParserException); + void parseError(const std::string& msg, bool eofException = false) override; /** Set the ANTLR3 lexer for this input. */ void setAntlr3Lexer(pANTLR3_LEXER pLexer); diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index bc16d646e..c35d8d963 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -40,8 +40,7 @@ class CvcInput : public AntlrInput { /** The ANTLR3 CVC parser for the input. */ pCvcParser d_pCvcParser; -public: - + public: /** Create an input. * * @param inputStream the input to parse @@ -52,18 +51,18 @@ public: virtual ~CvcInput(); /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { + InputLanguage getLanguage() const override + { return language::input::LANG_CVC4; } -protected: - + protected: /** Parse a command from the input. Returns NULL if there is * no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand(); + Command* parseCommand() override; /** Parse an expression from the input. Returns a null Expr * if there is no expression there to parse. @@ -72,8 +71,7 @@ protected: */ Expr parseExpr(); -private: - + private: /** Initialize the class. Called from the constructors once the input stream * is initialized. */ void init(); diff --git a/src/parser/input.cpp b/src/parser/input.cpp index c8c3c5e6d..b5f86d569 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -57,7 +57,7 @@ InputStream *Input::getInputStream() { Input* Input::newFileInput(InputLanguage lang, const std::string& filename, bool useMmap) - throw (InputStreamException) { +{ AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename, useMmap); return AntlrInput::newInput(lang, *inputStream); @@ -67,7 +67,7 @@ Input* Input::newStreamInput(InputLanguage lang, std::istream& input, const std::string& name, bool lineBuffered) - throw (InputStreamException) { +{ AntlrInputStream *inputStream = AntlrInputStream::newStreamInputStream(input, name, lineBuffered); return AntlrInput::newInput(lang, *inputStream); @@ -76,7 +76,7 @@ Input* Input::newStreamInput(InputLanguage lang, Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) - throw (InputStreamException) { +{ AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name); return AntlrInput::newInput(lang, *inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index b41d8a898..76e4ac17e 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -38,10 +38,8 @@ class FunctionType; namespace parser { class CVC4_PUBLIC InputStreamException : public Exception { - -public: + public: InputStreamException(const std::string& msg); - virtual ~InputStreamException() throw() { } }; /** Wrapper around an input stream. */ @@ -54,16 +52,14 @@ class CVC4_PUBLIC InputStream { * delete on exit. */ bool d_fileIsTemporary; -protected: - + protected: /** Initialize the input stream with a name. */ InputStream(std::string name, bool isTemporary=false) : d_name(name), d_fileIsTemporary(isTemporary) { } -public: - + public: /** Destructor. */ virtual ~InputStream() { if( d_fileIsTemporary ) { @@ -97,8 +93,7 @@ class CVC4_PUBLIC Input { Input(const Input& input) CVC4_UNDEFINED; Input& operator=(const Input& input) CVC4_UNDEFINED; -public: - + public: /** Create an input for the given file. * * @param lang the input language @@ -107,8 +102,7 @@ public: */ static Input* newFileInput(InputLanguage lang, const std::string& filename, - bool useMmap = false) - throw (InputStreamException); + bool useMmap = false); /** Create an input for the given stream. * @@ -122,8 +116,7 @@ public: static Input* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name, - bool lineBuffered = false) - throw (InputStreamException); + bool lineBuffered = false); /** Create an input for the given string * @@ -133,23 +126,17 @@ public: */ static Input* newStringInput(InputLanguage lang, const std::string& input, - const std::string& name) - throw (InputStreamException); - + const std::string& name); /** Destructor. Frees the input stream and closes the input. */ virtual ~Input(); /** Get the language that this Input is reading. */ - virtual InputLanguage getLanguage() const throw() = 0; + virtual InputLanguage getLanguage() const = 0; /** Retrieve the name of the input stream */ - const std::string getInputStreamName(){ - return getInputStream()->getName(); - } - -protected: - + const std::string getInputStreamName() { return getInputStream()->getName(); } + protected: /** Create an input. * * @param inputStream the input stream @@ -175,8 +162,8 @@ protected: /** * Throws a ParserException with the given message. */ - virtual void parseError(const std::string& msg, bool eofException = false) - throw (ParserException) = 0; + virtual void parseError(const std::string& msg, + bool eofException = false) = 0; /** Parse an expression from the input by invoking the * implementation-specific parsing method. Returns a null diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 0d8cc1fcb..395f41ba1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -518,8 +518,10 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { } void Parser::checkDeclaration(const std::string& varName, - DeclarationCheck check, SymbolType type, - std::string notes) throw(ParserException) { + DeclarationCheck check, + SymbolType type, + std::string notes) +{ if (!d_checksEnabled) { return; } @@ -549,7 +551,8 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunctionLike(Expr fun) throw(ParserException) { +void Parser::checkFunctionLike(Expr fun) +{ if (d_checksEnabled && !isFunctionLike(fun)) { stringstream ss; ss << "Expecting function-like symbol, found '"; @@ -559,7 +562,8 @@ void Parser::checkFunctionLike(Expr fun) throw(ParserException) { } } -void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) { +void Parser::checkArity(Kind kind, unsigned numArgs) +{ if (!d_checksEnabled) { return; } @@ -581,7 +585,8 @@ void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) { } } -void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) { +void Parser::checkOperator(Kind kind, unsigned numArgs) +{ if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) { parseError("Operator is not defined in the current logic: " + kindToString(kind)); @@ -592,9 +597,8 @@ void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) { void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); } void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } - -Command* Parser::nextCommand() throw(ParserException, - UnsafeInterruptException) { +Command* Parser::nextCommand() +{ Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; if (!d_commandQueue.empty()) { @@ -627,7 +631,8 @@ Command* Parser::nextCommand() throw(ParserException, return cmd; } -Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { +Expr Parser::nextExpression() +{ Debug("parser") << "nextExpression()" << std::endl; const Options& options = d_exprManager->getOptions(); d_resourceManager->spendResource(options.getParseStep()); diff --git a/src/parser/parser.h b/src/parser/parser.h index f2044c7ef..7f64b9580 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -400,9 +400,10 @@ public: * @param notes notes to add to a parse error (if one is generated) * @throws ParserException if checks are enabled and the check fails */ - void checkDeclaration(const std::string& name, DeclarationCheck check, + void checkDeclaration(const std::string& name, + DeclarationCheck check, SymbolType type = SYM_VARIABLE, - std::string notes = "") throw(ParserException); + std::string notes = ""); /** * Reserve a symbol at the assertion level. @@ -418,7 +419,7 @@ public: * @throws ParserException if checks are enabled and fun is not * a function */ - void checkFunctionLike(Expr fun) throw(ParserException); + void checkFunctionLike(Expr fun); /** * Check that kind can accept numArgs arguments. @@ -428,7 +429,7 @@ public: * kind cannot be applied to numArgs * arguments. */ - void checkArity(Kind kind, unsigned numArgs) throw(ParserException); + void checkArity(Kind kind, unsigned numArgs); /** * Check that kind is a legal operator in the current @@ -439,7 +440,7 @@ public: * @throws ParserException if the parser mode is strict and the * operator kind has not been enabled */ - void checkOperator(Kind kind, unsigned numArgs) throw(ParserException); + void checkOperator(Kind kind, unsigned numArgs); /** Create a new CVC4 variable expression of the given type. * @@ -671,26 +672,21 @@ public: bool isPredicate(const std::string& name); /** Parse and return the next command. */ - Command* nextCommand() throw(ParserException, UnsafeInterruptException); + Command* nextCommand(); /** Parse and return the next expression. */ - Expr nextExpression() throw(ParserException, UnsafeInterruptException); + Expr nextExpression(); /** Issue a warning to the user. */ - inline void warning(const std::string& msg) { - d_input->warning(msg); - } - + void warning(const std::string& msg) { d_input->warning(msg); } /** Issue a warning to the user, but only once per attribute. */ void attributeNotSupported(const std::string& attr); /** Raise a parse error with the given message. */ - inline void parseError(const std::string& msg) throw(ParserException) { - d_input->parseError(msg); - } - + inline void parseError(const std::string& msg) { d_input->parseError(msg); } /** Unexpectedly encountered an EOF */ - inline void unexpectedEOF(const std::string& msg) throw(ParserException) { + inline void unexpectedEOF(const std::string& msg) + { d_input->parseError(msg, true); } @@ -708,7 +704,8 @@ public: * support parsing quantifiers (just not doing anything with them). * So this mechanism gives you a way to do it with --parse-only. */ - inline void unimplementedFeature(const std::string& msg) throw(ParserException) { + inline void unimplementedFeature(const std::string& msg) + { if(!d_parseOnly) { parseError("Unimplemented feature: " + msg); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index ec8d4949d..ceda2ba47 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -65,7 +65,7 @@ void ParserBuilder::init(ExprManager* exprManager, } Parser* ParserBuilder::build() - throw (InputStreamException) { +{ Input* input = NULL; switch( d_inputType ) { case FILE_INPUT: diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 4b4eb4e4e..fe4a754d1 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -97,7 +97,7 @@ public: const Options& options); /** Build the parser, using the current settings. */ - Parser *build() throw (InputStreamException); + Parser* build(); /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h index c5a3d312e..7577b7bff 100644 --- a/src/parser/smt1/smt1_input.h +++ b/src/parser/smt1/smt1_input.h @@ -54,19 +54,19 @@ public: virtual ~Smt1Input(); /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { + InputLanguage getLanguage() const override + { return language::input::LANG_SMTLIB_V1; } -protected: - + protected: /** * Parse a command from the input. Returns NULL if * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand(); + Command* parseCommand() override; /** * Parse an expression from the input. Returns a null @@ -76,8 +76,7 @@ protected: */ Expr parseExpr(); -private: - + private: /** * Initialize the class. Called from the constructors once the input * stream is initialized. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 4832fc6b5..94bc03235 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -278,9 +278,11 @@ public: * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. */ - void checkDeclaration(const std::string& name, DeclarationCheck check, + void checkDeclaration(const std::string& name, + DeclarationCheck check, SymbolType type = SYM_VARIABLE, - std::string notes = "") throw(ParserException) { + std::string notes = "") + { // if the symbol is something like "-1", we'll give the user a helpful // syntax hint. (-1 is a valid identifier in SMT-LIB, NOT unary minus.) if( check != CHECK_DECLARED || @@ -304,7 +306,8 @@ public: this->Parser::checkDeclaration(name, check, type, ss.str()); } - void checkOperator(Kind kind, unsigned numArgs) throw(ParserException) { + void checkOperator(Kind kind, unsigned numArgs) + { Parser::checkOperator(kind, numArgs); // strict SMT-LIB mode enables extra checks for some bitvector operators // that CVC4 permits as N-ary but the standard requires is binary @@ -328,7 +331,8 @@ public: } // Throw a ParserException with msg appended with the current logic. - inline void parseErrorLogic(const std::string& msg) throw(ParserException) { + inline void parseErrorLogic(const std::string& msg) + { const std::string withLogic = msg + getLogic().getLogicString(); parseError(withLogic); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 4d6168643..0acb5462d 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -53,8 +53,7 @@ class Smt2Input : public AntlrInput { */ void init(); -public: - + public: /** * Create an input. * @@ -67,22 +66,18 @@ public: virtual ~Smt2Input(); /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { - return d_lang; - } - + InputLanguage getLanguage() const override { return d_lang; } /** Set the language that this Input is reading. */ void setLanguage(InputLanguage); -protected: - + protected: /** * Parse a command from the input. Returns NULL if * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand(); + Command* parseCommand() override; /** * Parse an expression from the input. Returns a null diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h index a66730ad6..0dca60a82 100644 --- a/src/parser/smt2/sygus_input.h +++ b/src/parser/smt2/sygus_input.h @@ -50,8 +50,7 @@ class SygusInput : public AntlrInput { */ void init(); -public: - + public: /** * Create an input. * @@ -63,19 +62,19 @@ public: virtual ~SygusInput(); /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { + InputLanguage getLanguage() const override + { return language::input::LANG_SYGUS; } -protected: - + protected: /** * Parse a command from the input. Returns NULL if * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand(); + Command* parseCommand() override; /** * Parse an expression from the input. Returns a null diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index a1f70641e..5dd56034d 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -50,8 +50,7 @@ class TptpInput : public AntlrInput { */ void init(); -public: - + public: /** * Create an input. * @@ -63,19 +62,19 @@ public: virtual ~TptpInput(); /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { + InputLanguage getLanguage() const override + { return language::input::LANG_TPTP; } -protected: - + protected: /** * Parse a command from the input. Returns NULL if * there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand(); + Command* parseCommand() override; /** * Parse an expression from the input. Returns a null