diff options
| -rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 10 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 2 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/PCLoggingSolver.cpp | 2 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 2 | ||||
| -rw-r--r-- | unittests/Expr/ExprTest.cpp | 8 | ||||
| -rw-r--r-- | unittests/Solver/SolverTest.cpp | 5 |
7 files changed, 18 insertions, 15 deletions
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 831a4d91..e3a83f9a 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -167,7 +167,9 @@ private: // Special case empty list. if (!head) { - PC << "arr" << updates.root->id; + // FIXME: We need to do something (assert, mangle, etc.) so that printing + // distinct arrays with the same name doesn't fail. + PC << updates.root->name; return; } @@ -217,7 +219,7 @@ private: if (openedList) PC << ']'; - PC << " @ arr" << updates.root->id; + PC << " @ " << updates.root->name; } void printWidth(PrintContext &PC, ref<Expr> e) { @@ -528,7 +530,7 @@ void ExprPPrinter::printQuery(std::ostream &os, ie = p.usedArrays.end(); it != ie; ++it) { const Array *A = *it; // FIXME: Print correct name, domain, and range. - PC << "array " << "arr" << A->id + PC << "array " << A->name << "[" << A->size << "]" << " : " << "w32" << " -> " << "w8" << " = symbolic"; @@ -572,7 +574,7 @@ void ExprPPrinter::printQuery(std::ostream &os, PC.breakLine(indent - 1); PC << '['; for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) { - PC << "arr" << (*it)->id; + PC << (*it)->name; if (it + 1 != evalArraysEnd) PC.breakLine(indent); } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 77596727..8c18fe73 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -1557,7 +1557,7 @@ Decl::Decl(DeclKind _Kind) : Kind(_Kind) {} void ArrayDecl::dump() { // FIXME: For now, print using the Array* "name". - std::cout << "array " << "arr" << Root->id + std::cout << "array " << Root->name << "[" << Size << "]" << " : " << 'w' << Domain << " -> " << 'w' << Range << " = "; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 7ebee1c7..69f9567c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -131,7 +131,7 @@ public: os << ", "; } - os << "MO" << array->id; + os << "MO" << array->name; } for (elements_ty::const_iterator it = elements.begin(), ie = elements.end(); it != ie; ++it) { @@ -144,7 +144,7 @@ public: os << ", "; } - os << "MO" << array->id << " : " << dis; + os << "MO" << array->name << " : " << dis; } os << "}"; } diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp index 3c605256..03146251 100644 --- a/lib/Solver/PCLoggingSolver.cpp +++ b/lib/Solver/PCLoggingSolver.cpp @@ -128,7 +128,7 @@ public: e = objects.end(); i != e; ++i, ++values_it) { const Array *array = *i; std::vector<unsigned char> &data = *values_it; - os << "# arr" << array->id << " = ["; + os << "# " << array->name << " = ["; for (unsigned j = 0; j < array->size; j++) { os << (int) data[j]; if (j+1 < array->size) diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index a575c086..fca83905 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -171,7 +171,7 @@ static bool EvaluateInputAST(const char *Filename, for (unsigned i = 0, e = result.size(); i != e; ++i) { llvm::cout << "\tArray " << i << ":\t" - << "arr" << QC->Objects[i]->id + << QC->Objects[i]->name << "["; for (unsigned j = 0; j != QC->Objects[i]->size; ++j) { llvm::cout << (unsigned) result[i][j]; diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index 7b37973a..f86af1aa 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -28,9 +28,9 @@ TEST(ExprTest, BasicConstruction) { } TEST(ExprTest, ConcatExtract) { - Array *array = new Array(0, 1, 256); + Array *array = new Array("arr0", 0, 1, 256); ref<Expr> read8 = Expr::createTempRead(array, 8); - Array *array2 = new Array(0, 2, 256); + Array *array2 = new Array("arr1", 0, 2, 256); ref<Expr> read8_2 = Expr::createTempRead(array2, 8); ref<Expr> c100 = getConstant(100, 8); @@ -80,10 +80,10 @@ TEST(ExprTest, ConcatExtract) { } TEST(ExprTest, ExtractConcat) { - Array *array = new Array(0, 3, 256); + Array *array = new Array("arr0", 0, 3, 256); ref<Expr> read64 = Expr::createTempRead(array, 64); - Array *array2 = new Array(0, 4, 256); + Array *array2 = new Array("arr1", 0, 4, 256); ref<Expr> read8_2 = Expr::createTempRead(array2, 8); ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4); diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 1b1e0f3f..a6130716 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -12,6 +12,7 @@ #include "klee/Constraints.h" #include "klee/Expr.h" #include "klee/Solver.h" +#include "llvm/ADT/StringExtras.h" using namespace klee; @@ -43,8 +44,8 @@ void testOperation(Solver &solver, return; unsigned size = Expr::getMinBytesForWidth(operandWidth); - static unsigned id = 0; - Array *array = new Array(0, ++id, size); + static uint64_t id = 0; + Array *array = new Array("arr" + llvm::utostr(id), 0, ++id, size); symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, operandWidth))); } |