From f3bca68c8e5e5362ea247c582e7e9ff1e717e9d2 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Sat, 11 Jul 2009 00:08:29 +0000
Subject: 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
---
 lib/SMT/SMTParser.cpp |  6 ++++--
 lib/SMT/smtlib.y      | 19 +++++++++++--------
 2 files changed, 15 insertions(+), 10 deletions(-)

(limited to 'lib/SMT')

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
     }
 
-- 
cgit 1.4.1