From 70b406696b6cc4c1c3c13f7d50ec1fe083a4fa5b Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 1 Mar 2016 15:25:45 +0100 Subject: 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. --- lib/Expr/ExprPPrinter.cpp | 22 ++++++++++++++++------ 1 file 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::iterator it = p.usedArrays.begin(), - ie = p.usedArrays.end(); it != ie; ++it) { + std::vector sortedArray(p.usedArrays.begin(), + p.usedArrays.end()); + std::sort(sortedArray.begin(), sortedArray.end(), ArrayPtrsByName()); + for (std::vector::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 { -- cgit 1.4.1