Wrote a new SMTParser that inherits from klee::expr::Parser.

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

2 files changed, 97 insertions, 0 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
new file mode 100644
index 00000000..b87bbdbc
--- /dev/null
+++ b/lib/SMT/SMTParser.cpp
@@ -0,0 +1,49 @@
+//===-- SMTParser.cpp -----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "parser_temp.h"
+#include "SMTParser.h"
+#include "expr/Parser.h"
+
+#include <iostream>
+#include <fstream>
+#include <cstring>
+
+using namespace std;
+using namespace klee;
+using namespace klee::expr;
+
+extern int smtlibparse(); 
+extern void *smtlib_createBuffer(int);
+extern void smtlib_deleteBuffer(void *);
+extern void smtlib_switchToBuffer(void *);
+extern int smtlib_bufSize(void);
+extern void smtlib_setInteractive(bool);
+
+namespace CVC3 {
+  ParserTemp* parserTemp;
+}
+
+void SMTParser::Init() {
+  cout << "Initializing parser\n";
+  void *buf = smtlib_createBuffer(smtlib_bufSize());
+
+  CVC3::parserTemp = new CVC3::ParserTemp();
+  CVC3::parserTemp->fileName = fname;
+  CVC3::parserTemp->is = new ifstream(fname.c_str());
+  CVC3::parserTemp->interactive = false;
+  
+  smtlib_switchToBuffer(buf);
+  smtlib_setInteractive(false);
+  smtlibparse();
+}
+
+Decl* SMTParser::ParseTopLevelDecl() {
+  return NULL;
+}
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
new file mode 100644
index 00000000..5abbee7b
--- /dev/null
+++ b/lib/SMT/SMTParser.h
@@ -0,0 +1,48 @@
+//===-- SMTParser.h -------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+
+#ifndef SMT_PARSER_H
+#define SMT_PARSER_H
+
+#include "parser_temp.h"
+#include "expr/Parser.h"
+
+#include <cassert>
+#include <iostream>
+#include <map>
+#include <cstring>
+
+namespace klee {
+namespace expr {
+
+class SMTParser : public klee::expr::Parser {
+ private:
+  std::string fname;
+  void *buf;
+
+ public:
+  SMTParser(const std::string filename) : fname(filename) {}
+  
+  virtual klee::expr::Decl *ParseTopLevelDecl();
+  
+  virtual void SetMaxErrors(unsigned N) { }
+  
+  virtual unsigned GetNumErrors() const {  return 1; }
+  
+  virtual ~SMTParser() {}
+  
+  void Init(void);
+};
+
+}
+}
+
+#endif
+