Changed expression nodes to be ExprHandle (instead of ExprHandle*), and

added a quick hack to change Bison unions to structs. 



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

5 files changed, 18 insertions, 12 deletions

diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile
index 5ab2d16f..92ec8018 100644
--- a/lib/SMT/Makefile
+++ b/lib/SMT/Makefile
@@ -14,10 +14,14 @@ include $(LEVEL)/Makefile.common
 
 smtlib_parser.cpp smtlib_parser.h: smtlib.y
 	bison -d -o smtlib_parser.cpp -p smtlib smtlib.y
-	mv smtlib_parser.hpp smtlib_parser.h
+	mv smtlib_parser.hpp smtlib_parser.h	
+	perl -pi -e 's/union/struct/g' smtlib_parser.cpp
+	perl -pi -e 's/union/struct/g' smtlib_parser.h
+
 
 smtlib_lexer.cpp: smtlib.lex smtlib_parser.h
 	flex -I -Psmtlib -osmtlib_lexer.cpp smtlib.lex
+	perl -pi -e 's/union/struct/g' smtlib_lexer.cpp
 
 .PHONY: regen
 regen: smtlib_lexer.cpp smtlib_parser.cpp smtlib_parser.h
diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp
index 9284d7d0..439e189c 100644
--- a/lib/SMT/parser.cpp
+++ b/lib/SMT/parser.cpp
@@ -120,7 +120,7 @@ namespace CVC3 {
   }
     
 
-  klee::expr::ExprHandle* Parser::next() {
+  klee::expr::ExprHandle Parser::next() {
     // If no more commands are available, return a Null Expr
     if(d_data->temp.done) return NULL;//Expr();
     // Set the global var so the parser uses the right stream and EM
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
index c061841f..30a01ac2 100644
--- a/lib/SMT/parser.h
+++ b/lib/SMT/parser.h
@@ -48,7 +48,7 @@ namespace CVC3 {
     // Destructor
     ~Parser();
     // Read the next command.  
-    klee::expr::ExprHandle* next();
+    klee::expr::ExprHandle next();
     // Check if we are done (end of input has been reached)
     bool done() const;
     // The same check can be done by using the class Parser's value as
diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h
index afd8af21..704157d9 100644
--- a/lib/SMT/parser_temp.h
+++ b/lib/SMT/parser_temp.h
@@ -47,7 +47,7 @@ namespace CVC3 {
     // File name
     std::string fileName;
     // The last parsed Expr
-    klee::expr::ExprHandle* expr;
+    klee::expr::ExprHandle expr;
     // Whether we are done or not
     bool done;
     // Whether we are running interactive
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index be1c5143..72185a93 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -23,8 +23,11 @@
    commands in SMT-LIB language.
 */
 
-//#include "vc.h"
 #include "parser_temp.h"
+#include "klee/Expr.h"
+
+using namespace klee;
+using namespace klee::expr;
 
 // Exported shared data
 namespace CVC3 {
@@ -75,9 +78,7 @@ int smtliberror(const char *s)
 
 %union {
   std::string *str;
-  std::vector<std::string> *strvec;
-  klee::expr::ExprHandle* node;
-  std::vector<void*> *vec;
+  klee::expr::ExprHandle node;
 };
 
 
@@ -176,13 +177,14 @@ benchmark:
       $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4));
       delete $4;
       */
-      $$ = NULL;
+      $$ = $4;
     }
   | EOF_TOK
     { 
       TMP->done = true;
       //$$ = new CVC3::Expr();
-      $$ = NULL;
+      //$$ = ConstantExpr::create(1, 1);
+      $$ = ExprHandle();
     }
 ;
 
@@ -761,12 +763,12 @@ prop_atom:
     TRUE_TOK
     {
       //$$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
-      $$ = NULL;
+      $$ = ConstantExpr::create(1, 1);
     }
   | FALSE_TOK
     { 
       //$$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
-      $$ = NULL;
+      $$ = ConstantExpr::create(0, 1);;
     }
 /*
   | fvar