diff options
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/Cvc.g | 35 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 8 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 4 |
3 files changed, 26 insertions, 21 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4577b504c..b496aa91c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) { case IN_TOK: return 33; default: - Unhandled(CvcParserTokenNames[type]); + std::stringstream ss; + ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); } }/* getOperatorPrecedence() */ @@ -318,16 +320,18 @@ Kind getOperatorKind(int type, bool& negate) { case INTDIV_TOK: return kind::INTS_DIVISION; case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; - case EXP_TOK: Unhandled(CvcParserTokenNames[type]); + case EXP_TOK: break; // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; case BAR: return kind::BITVECTOR_OR; case BVAND_TOK: return kind::BITVECTOR_AND; - - default: - Unhandled(CvcParserTokenNames[type]); } + + std::stringstream ss; + ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); + }/* getOperatorKind() */ unsigned findPivot(const std::vector<unsigned>& operators, @@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector<CVC4::Expr>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { - Assert(expressions.size() == operators.size() + 1); - Assert(startIndex < expressions.size()); - Assert(stopIndex < expressions.size()); - Assert(startIndex <= stopIndex); + assert(expressions.size() == operators.size() + 1); + assert(startIndex < expressions.size()); + assert(stopIndex < expressions.size()); + assert(startIndex <= stopIndex); if(stopIndex == startIndex) { return expressions[startIndex]; @@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { #include <stdint.h> +#include <cassert> #include "expr/command.h" #include "parser/parser.h" #include "util/subrange_bound.h" @@ -1016,7 +1021,7 @@ type[CVC4::Type& t, /* a type, possibly a function */ : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { - Assert(t.isTuple()); + assert(t.isTuple()); args = TupleType(t).getTypes(); } else { args.push_back(t); @@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f] } : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ ASSIGN_TOK uminusTerm[f3] - { Assert(dims.size() >= 1); + { assert(dims.size() >= 1); // these loops are a bit complicated; they're only used for the // multidimensional ...WITH [a][b] :=... syntax for(unsigned i = 0; i < dims.size() - 1; ++i) { @@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f] } else if(t.isTester()) { f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); } else { - Unhandled(t); + PARSER_STATE->parseError("internal error: unhandled function application kind"); } } @@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f] | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); f = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN { std::vector< std::pair<std::string, Type> > typeIds; - Assert(names.size() == args.size()); + assert(names.size() == args.size()); for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index d91a13bee..26ee4a693 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -32,7 +32,7 @@ namespace parser { CvcInput::CvcInput(AntlrInputStream& inputStream) : AntlrInput(inputStream,6) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); if( d_pCvcLexer == NULL ) { @@ -42,7 +42,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pCvcParser = CvcParserNew(tokenStream); if( d_pCvcParser == NULL ) { @@ -59,12 +59,12 @@ CvcInput::~CvcInput() { } Command* CvcInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseCommand(d_pCvcParser); } Expr CvcInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 9a1f24fde..94e1bfc60 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -66,7 +66,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** Parse an expression from the input. Returns a null <code>Expr</code> * if there is no expression there to parse. @@ -74,7 +74,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); private: |