Report an error in the SMT parser when encountering the few operators

not supported yet: bvneg, bvsmod, bvxnor, rotate_left, rotate_right,
repeat.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75319 91177308-0d34-0410-b5e6-96231b3b80d8

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
     }