aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2009-06-10 09:13:20 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2009-06-10 09:13:20 +0000
commit930bf13e988c169c585da158c4410bdb49cc5ec6 (patch)
treee681646e5859bdb400c44981d92b30825548e32c /lib
parentf029d8ad70310b400612d85e60e8925101194e32 (diff)
downloadklee-930bf13e988c169c585da158c4410bdb49cc5ec6.tar.gz
Removed CVC3's Parser class.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73166 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib')
-rw-r--r--lib/SMT/parser.cpp151
1 files changed, 0 insertions, 151 deletions
diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp
deleted file mode 100644
index 439e189c..00000000
--- a/lib/SMT/parser.cpp
+++ /dev/null
@@ -1,151 +0,0 @@
-/*****************************************************************************/
-/*!
- * \file parser.cpp
- * \brief The top-level API to the parser. See parser.h for details.
- *
- * Author: Sergey Berezin
- *
- * Created: Wed Feb 5 11:46:57 2003
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- *
- * <hr>
- *
- */
-/*****************************************************************************/
-
-#include <fstream>
-#include <iomanip>
-#include <iostream>
-#include <stdlib.h>
-#include "parser_temp.h"
-#include "parser.h"
-
-using namespace std;
-
-// The communication entry points of the actual parsers
-
-// for smtlib language (smtlib.y and smtlib.lex)
-extern int smtlibparse();
-extern void *smtlib_createBuffer(int);
-extern void smtlib_deleteBuffer(void *);
-extern void smtlib_switchToBuffer(void *);
-extern int smtlib_bufSize();
-extern void *smtlibBufState();
-void smtlib_setInteractive(bool);
-
-namespace CVC3 {
-
- // The global pointer to ParserTemp. Each instance of class Parser
- // sets this pointer before any calls to the lexer. We do it this
- // way because flex and bison use global vars, and we want each
- // Parser object to appear independent.
-
- // FIXME: This should probably go away eventually, when I figure out
- // flex++ -- Sergey.
- ParserTemp* parserTemp;
-
- int ParserTemp::error(const string& s) {
- // FIXME: Fail better?
- std::cerr << "error: " << s << "\n";
- exit(1);
- return 0;
- }
-
- // Internal storage class; I'll use member names without 'd_'s here
- class ParserData {
- public:
- // Is the input given by the file name or as istream?
- bool useName;
- ParserTemp temp;
- // Internal buffer used by the parser
- void* buffer;
- };
-
- // Constructors
- Parser::Parser(bool interactive, const std::string& fileName)
- : d_data(new ParserData) {
- if(fileName == "") {
- // Use std::cin
- d_data->useName = false;
- d_data->temp.is = &cin;
- d_data->temp.fileName = "stdin";
- d_data->temp.interactive = interactive;
- } else {
- // Open the file by name
- d_data->useName = true;
- d_data->temp.fileName = fileName;
- d_data->temp.is = new ifstream(fileName.c_str());
- if (!(*d_data->temp.is)) {
- // FIXME: Fail better?
- std::cerr << "error: File not found: " << fileName << "\n";
- exit(1);
- }
- d_data->temp.interactive = false;
- }
- initParser();
- }
-
- Parser::Parser(std::istream& is, bool interactive)
- : d_data(new ParserData) {
- d_data->useName = false;
- d_data->temp.is = &is;
- d_data->temp.fileName = "stdin";
- d_data->temp.interactive = interactive;
- initParser();
- }
-
- // Destructor
- Parser::~Parser() {
- if(d_data->useName) // Stream is ours; delete it
- delete d_data->temp.is;
- deleteParser();
- delete d_data;
- }
-
- // Initialize the actual parser
- void Parser::initParser() {
- d_data->buffer = smtlib_createBuffer(smtlib_bufSize());
- d_data->temp.lineNum = 1;
- }
-
- // Clean up the parser's internal data structures
- void Parser::deleteParser() {
- smtlib_deleteBuffer(d_data->buffer);
- }
-
-
- 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
- parserTemp = &(d_data->temp);
- // Switch to our buffer, in case there are multiple instances of
- // the parser running
- smtlib_switchToBuffer(d_data->buffer);
- smtlib_setInteractive(d_data->temp.interactive);
- smtlibparse();
- // Reset the prompt to the main one
- d_data->temp.setPrompt1();
- return d_data->temp.expr;
- }
-
- bool Parser::done() const { return d_data->temp.done; }
-
- void Parser::printLocation(ostream & out) const
- {
- out << d_data->temp.fileName << ":" << d_data->temp.lineNum;
- }
-
- void Parser::reset()
- {
- d_data->temp.expr = NULL;//Expr();
- }
-
-
-} // end of namespace CVC3