diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 09:54:15 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 09:54:15 -0400 |
commit | 3afbf810287fb3f1a99ef907f91f5e93c3b93226 (patch) | |
tree | 7272a8579e1dd49c18591b1edef64c9c8fad5609 /src/parser | |
parent | 36dd801660bad8fe1d967c887363f15dbe1bcc63 (diff) |
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places
Thanks to David Cok for reporting these issues.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.h | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 19 |
2 files changed, 12 insertions, 8 deletions
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; |