diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
commit | 010ad47b7b3e1909f31525fc45be2c27c1b72e45 (patch) | |
tree | b18bf9b0724c6418dc57bf0d15a9db351f6f252e /src/parser/parser.cpp | |
parent | c5177b11ad8cc5287fa7a8e65f78d5f6cfe23ead (diff) |
Give a more useful parse error message for "undeclared variable -1".
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index fa2a1e744..a7834a5aa 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -374,7 +374,8 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { void Parser::checkDeclaration(const std::string& varName, DeclarationCheck check, - SymbolType type) + SymbolType type, + std::string notes) throw(ParserException) { if(!d_checksEnabled) { return; @@ -384,14 +385,16 @@ void Parser::checkDeclaration(const std::string& varName, case CHECK_DECLARED: if( !isDeclared(varName, type) ) { parseError("Symbol " + varName + " not declared as a " + - (type == SYM_VARIABLE ? "variable" : "type")); + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); } break; case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { parseError("Symbol " + varName + " previously declared as a " + - (type == SYM_VARIABLE ? "variable" : "type")); + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); } break; |