blob: edc1258f461fd346a9f21c15f978cf6e72e1c9d1 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
//===-- 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 "expr/Parser.h"
#include <cassert>
#include <iostream>
#include <map>
#include <cstring>
namespace klee {
namespace expr {
class SMTParser : public klee::expr::Parser {
private:
void *buf;
public:
/* For interacting w/ the actual parser, should make this nicer */
static SMTParser* parserTemp;
std::string fileName;
std::istream* is;
int lineNum;
bool done;
bool arraysEnabled;
std::vector<ExprHandle> assumptions;
klee::expr::ExprHandle query;
int bvSize;
bool queryParsed;
SMTParser(const std::string filename);
virtual klee::expr::Decl *ParseTopLevelDecl();
virtual void SetMaxErrors(unsigned N) { }
virtual unsigned GetNumErrors() const { return 1; }
virtual ~SMTParser() {}
void Init(void);
int Error(const std::string& s);
};
}
}
#endif
|
