summaryrefslogtreecommitdiff
path: root/src/parser/cvc/Cvc.g
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-10-03 13:22:45 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-10-03 13:22:45 -0400
commit4fb42ac1e5a96c1633bb4570681b09db657f673d (patch)
tree7d2cc21a7ac9ab58e37cc1517ee1ed101c831d39 /src/parser/cvc/Cvc.g
parent4a69f126fb2301f8da2db3841e1362aacb59362c (diff)
Improve error in CVC parser in presence of unrecognized command name.
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r--src/parser/cvc/Cvc.g7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0a440f299..347759c9a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -635,6 +635,13 @@ command returns [CVC4::Command* cmd = NULL]
cmd = new EmptyCommand();
}
}
+ | IDENTIFIER SEMICOLON
+ { std::stringstream ss;
+ ss << "Unrecognized command `"
+ << AntlrInput::tokenText($IDENTIFIER)
+ << "'";
+ PARSER_STATE->parseError(ss.str());
+ }
;
typeOrVarLetDecl[CVC4::parser::DeclarationCheck check]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback