From: Morgan Deters Date: Fri, 17 May 2013 13:54:15 +0000 (-0400) Subject: Better error on illegal (pop N); also more compliant SMT-LIB error messages in some... X-Git-Tag: cvc5-1.0.0~7287^2~113^2~8 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3afbf810287fb3f1a99ef907f91f5e93c3b93226;p=cvc5.git Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places Thanks to David Cok for reporting these issues. --- diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 3376e9d0b..5c9f8af21 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -313,7 +313,11 @@ restart: line += "\n"; goto restart; } catch(ParserException& pe) { - d_out << pe << endl; + if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) { + d_out << "(error \"" << pe << "\")" << endl; + } else { + d_out << pe << endl; + } // We can't really clear out the sequence and abort the current line, // because the parse error might be for the second command on the // line. The first ones haven't yet been executed by the SmtEngine, diff --git a/src/main/main.cpp b/src/main/main.cpp index 7b61b48aa..a4c4b9c0a 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -37,10 +37,12 @@ #include "util/output.h" #include "util/result.h" #include "util/statistics.h" +#include "util/language.h" using namespace std; using namespace CVC4; using namespace CVC4::main; +using namespace CVC4::language; /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. @@ -64,7 +66,11 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; #endif - *opts[options::err] << "CVC4 Error:" << endl << e << endl; + if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) { + *opts[options::err] << "(error \"" << e << "\")" << endl; + } else { + *opts[options::err] << "CVC4 Error:" << endl << e << endl; + } if(opts[options::statistics] && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(*opts[options::err]); diff --git a/src/parser/parser.h b/src/parser/parser.h index 1ca56dc06..d13fbf2d6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -482,6 +482,7 @@ public: } } + inline size_t scopeLevel() const { return d_symtab->getLevel(); } inline void pushScope() { d_symtab->pushScope(); } inline void popScope() { d_symtab->popScope(); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6c98a5529..dbe1135b3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -284,7 +284,7 @@ command returns [CVC4::Command* cmd = NULL] { $cmd = new GetValueCommand(terms); } | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetAssignmentCommand; } + { cmd = new GetAssignmentCommand(); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[expr, expr2] @@ -294,13 +294,13 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new CheckSatCommand(MK_CONST(bool(true))); } | /* get-assertions */ GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetAssertionsCommand; } + { cmd = new GetAssertionsCommand(); } | /* get-proof */ GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetProofCommand; } + { cmd = new GetProofCommand(); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetUnsatCoreCommand; } + { cmd = new GetUnsatCoreCommand(); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL @@ -324,12 +324,15 @@ command returns [CVC4::Command* cmd = NULL] | { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?"); } else { - cmd = new PushCommand; + cmd = new PushCommand(); } } ) | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); + if(n > PARSER_STATE->scopeLevel()) { + PARSER_STATE->parseError("Attempted to pop above the top stack frame."); + } if(n == 0) { cmd = new EmptyCommand(); } else if(n == 1) { @@ -349,11 +352,11 @@ command returns [CVC4::Command* cmd = NULL] | { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?"); } else { - cmd = new PopCommand; + cmd = new PopCommand(); } } ) | EXIT_TOK - { cmd = new QuitCommand; } + { cmd = new QuitCommand(); } /* CVC4-extended SMT-LIB commands */ | extendedCommand[cmd] @@ -400,7 +403,7 @@ extendedCommand[CVC4::Command*& cmd] cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetModelCommand; } + { cmd = new GetModelCommand(); } | ECHO_TOK ( simpleSymbolicExpr[sexpr] { std::stringstream ss;