diff options
Diffstat (limited to 'lib/SMT')
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 6 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 19 |
2 files changed, 15 insertions, 10 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 96d33661..5edff9d0 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -63,8 +63,10 @@ Decl* SMTParser::ParseTopLevelDecl() { } // XXX: give more info -int SMTParser::Error(const string& s) { - std::cerr << "error: " << s << "\n"; +int SMTParser::Error(const string& msg) { + std::cerr << SMTParser::parserTemp->fileName << ":" + << SMTParser::parserTemp->lineNum + << ": " << msg << "\n"; exit(1); return 0; } diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index c169b4e0..0efc5703 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -51,10 +51,7 @@ extern int smtliblex(void); int smtliberror(const char *s) { - std::ostringstream ss; - ss << SMTParser::parserTemp->fileName << ":" << SMTParser::parserTemp->lineNum - << ": " << s; - return SMTParser::parserTemp->Error(ss.str()); + return SMTParser::parserTemp->Error(s); } @@ -625,9 +622,10 @@ an_pred: an_arithmetic_fun: - LPAREN_TOK BVNEG_TOK an_term an_term annotations + LPAREN_TOK BVNEG_TOK an_term annotations { - $$ = NULL; // XXX: not supported yet + smtliberror("bvneg not supported yet"); + $$ = NULL; // TODO } | LPAREN_TOK BVADD_TOK an_term an_term annotations @@ -667,7 +665,8 @@ an_arithmetic_fun: | LPAREN_TOK BVSMOD_TOK an_term an_term annotations { - $$ = NULL; // XXX: not supported yet + smtliberror("bvsmod not supported yet"); + $$ = NULL; // TODO } ; @@ -695,7 +694,8 @@ an_bitwise_fun: | LPAREN_TOK BVXNOR_TOK an_term an_term annotations { - $$ = NULL; // TODO + smtliberror("bvxnor not supported yet"); + $$ = NULL; // TODO } | LPAREN_TOK BVSHL_TOK an_term an_term annotations @@ -715,11 +715,13 @@ an_bitwise_fun: | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations { + smtliberror("rotate_left not supported yet"); $$ = NULL; // TODO } | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations { + smtliberror("rotate_right not supported yet"); $$ = NULL; // TODO } @@ -740,6 +742,7 @@ an_bitwise_fun: | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations { + smtliberror("repeat not supported yet"); $$ = NULL; // TODO } |