diff options
Diffstat (limited to 'lib/SMT')
-rw-r--r-- | lib/SMT/SMTParser.cpp | 11 | ||||
-rw-r--r-- | lib/SMT/SMTParser.h | 2 | ||||
-rw-r--r-- | lib/SMT/main.cpp | 3 | ||||
-rw-r--r-- | lib/SMT/smtlib.y | 2 |
4 files changed, 5 insertions, 13 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 22578f46..03042fdd 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -14,7 +14,6 @@ #include "klee/Constraints.h" #include "expr/Parser.h" -#include <iostream> #include <fstream> #include <string> #include <sstream> @@ -23,7 +22,6 @@ //#define DEBUG -using namespace std; using namespace klee; using namespace klee::expr; @@ -103,9 +101,8 @@ bool SMTParser::Solve() { // XXX: give more info int SMTParser::Error(const string& msg) { - std::cerr << SMTParser::parserTemp->fileName << ":" - << SMTParser::parserTemp->lineNum - << ": " << msg << "\n"; + llvm::errs() << SMTParser::parserTemp->fileName << ":" + << SMTParser::parserTemp->lineNum << ": " << msg << "\n"; exit(1); return 0; } @@ -213,7 +210,7 @@ void SMTParser::AddVar(std::string name, ExprHandle val) { ExprHandle SMTParser::GetVar(std::string name) { VarEnv top = varEnvs.top(); if (top.find(name) == top.end()) { - std::cerr << "Cannot find variable ?" << name << "\n"; + llvm::errs() << "Cannot find variable ?" << name << "\n"; exit(1); } return top[name]; @@ -241,7 +238,7 @@ void SMTParser::AddFVar(std::string name, ExprHandle val) { ExprHandle SMTParser::GetFVar(std::string name) { FVarEnv top = fvarEnvs.top(); if (top.find(name) == top.end()) { - std::cerr << "Cannot find fvar $" << name << "\n"; + llvm::errs() << "Cannot find fvar $" << name << "\n"; exit(1); } return top[name]; diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index fd1ec044..ac84e74c 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -13,8 +13,6 @@ #include "expr/Parser.h" -#include <cassert> -#include <iostream> #include <map> #include <stack> #include <string> diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 034c4ce4..31fa311d 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -2,9 +2,6 @@ #include "klee/ExprBuilder.h" -#include <iostream> - -using namespace std; using namespace klee; int main(int argc, char** argv) { diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 01d3539d..eb3b3890 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -254,7 +254,7 @@ bench_attribute: | COLON_TOK LOGIC_TOK logic_name { if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") { - std::cerr << "ERROR: Logic " << *$3 << " not supported."; + llvm::errs() << "ERROR: Logic " << *$3 << " not supported."; exit(1); } |