aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/SMT/SMTParser.cpp17
-rw-r--r--lib/SMT/main.cpp2
-rw-r--r--lib/SMT/smtlib.y1
3 files changed, 16 insertions, 4 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index d3a8c9ea..96d33661 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -17,6 +17,8 @@
#include <cassert>
#include <stack>
+//#define DEBUG
+
using namespace std;
using namespace klee;
using namespace klee::expr;
@@ -50,7 +52,7 @@ void SMTParser::Init() {
smtlib_switchToBuffer(buf);
smtlib_setInteractive(false);
smtlibparse();
- cout << "Parsed successfully.\n";
+ //xcout << "Parsed successfully.\n";
}
Decl* SMTParser::ParseTopLevelDecl() {
@@ -121,7 +123,9 @@ void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
exit(1);
}
+#ifdef DEBUG
std::cout << "Declaring " << name << " of width " << w << "\n";
+#endif
Array *arr = new Array(name, w / 8);
@@ -137,7 +141,6 @@ void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
- cerr << "In GetConstExpr(): val=" << val << ", base=" << (unsigned)base << ", width=" << w << "\n";
assert(base == 2 || base == 10 || base == 16);
llvm::APInt ap(w, val.c_str(), val.length(), base);
@@ -146,17 +149,23 @@ ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Wi
void SMTParser::PushVarEnv() {
+#ifdef DEBUG
cout << "Pushing new var env\n";
+#endif
varEnvs.push(VarEnv(varEnvs.top()));
}
void SMTParser::PopVarEnv() {
+#ifdef DEBUG
cout << "Popping var env\n";
+#endif
varEnvs.pop();
}
void SMTParser::AddVar(std::string name, ExprHandle val) {
+#ifdef DEBUG
cout << "Adding (" << name << ", " << val << ") to current var env.\n";
+#endif
varEnvs.top()[name] = val;
}
@@ -175,12 +184,16 @@ void SMTParser::PushFVarEnv() {
}
void SMTParser::PopFVarEnv(void) {
+#ifdef DEBUG
cout << "Popping fvar env\n";
+#endif
fvarEnvs.pop();
}
void SMTParser::AddFVar(std::string name, ExprHandle val) {
+#ifdef DEBUG
cout << "Adding (" << name << ", " << val << ") to current fvar env.\n";
+#endif
fvarEnvs.top()[name] = val;
}
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index d5137782..38bfac86 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -14,5 +14,5 @@ int main(int argc, char** argv) {
smtParser.Init();
- cout << "Query: " << smtParser.query << "\n";
+ cout << smtParser.query << "\n";
}
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 43682cf4..c169b4e0 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -848,7 +848,6 @@ basic_term:
}
| symb
{
- std::cout << "SYMBOL " << *$1 << "\n";
$$ = PARSER->GetVar(*$1);
}
;