about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2009-07-10 23:30:46 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2009-07-10 23:30:46 +0000
commitefeba0da263aa4c2feb2606e9d0dbf076ac48087 (patch)
tree770bfda552bf0d0febdd6deaba4639a64c41b7d7 /lib/SMT
parent304b19cbeaea3e47064e6fb4faeb6e880bd1c574 (diff)
downloadklee-efeba0da263aa4c2feb2606e9d0dbf076ac48087.tar.gz
Removed debug info.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75313 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT')
-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);
     }
 ;