about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-01 15:25:45 +0100
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-22 15:21:47 +0100
commit70b406696b6cc4c1c3c13f7d50ec1fe083a4fa5b (patch)
treeb5c6ad37cb53e8b0364a98aa5bb10d91c3229c3c
parent007d1ee02dae61bdb0760097a700d21968514b94 (diff)
downloadklee-70b406696b6cc4c1c3c13f7d50ec1fe083a4fa5b.tar.gz
ExprPPrinter: Print out arrays deterministically
The address of KLEE-internal data structures should not influence the
order arrays are printed out.
Order arrays by name.
-rw-r--r--lib/Expr/ExprPPrinter.cpp22
1 files changed, 16 insertions, 6 deletions
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index ddcc57a1..1682d9b5 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -457,6 +457,14 @@ void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
+namespace {
+
+struct ArrayPtrsByName {
+  bool operator()(const Array *a1, const Array *a2) const {
+    return a1->name < a2->name;
+  }
+};
+}
 
 void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const ConstraintManager &constraints,
@@ -482,13 +490,15 @@ void ExprPPrinter::printQuery(llvm::raw_ostream &os,
   if (printArrayDecls) {
     for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it)
       p.usedArrays.insert(*it);
-    for (std::set<const Array*>::iterator it = p.usedArrays.begin(), 
-           ie = p.usedArrays.end(); it != ie; ++it) {
+    std::vector<const Array *> sortedArray(p.usedArrays.begin(),
+                                           p.usedArrays.end());
+    std::sort(sortedArray.begin(), sortedArray.end(), ArrayPtrsByName());
+    for (std::vector<const Array *>::iterator it = sortedArray.begin(),
+                                              ie = sortedArray.end();
+         it != ie; ++it) {
       const Array *A = *it;
-      // FIXME: Print correct name, domain, and range.
-      PC << "array " << A->name
-         << "[" << A->size << "]"
-         << " : " << "w32" << " -> " << "w8" << " = ";
+      PC << "array " << A->name << "[" << A->size << "]"
+         << " : w" << A->domain << " -> w" << A->range << " = ";
       if (A->isSymbolicArray()) {
         PC << "symbolic";
       } else {