diff options
author | Eric Rizzi <eric.rizzi@gmail.com> | 2015-09-14 14:32:37 -0400 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2016-11-23 20:36:44 +0000 |
commit | f27cf86466d75c71a302abe5e0a3ffcad1670373 (patch) | |
tree | dd598d703d01fc8292afa6cc56816ec822715923 /lib/Solver/PCLoggingSolver.cpp | |
parent | 094a21832d94bfaa5da8ea667e646328ca0e5432 (diff) | |
download | klee-f27cf86466d75c71a302abe5e0a3ffcad1670373.tar.gz |
Renamed .pc to .kquery (kleaver query)
Diffstat (limited to 'lib/Solver/PCLoggingSolver.cpp')
-rw-r--r-- | lib/Solver/PCLoggingSolver.cpp | 68 |
1 files changed, 0 insertions, 68 deletions
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp deleted file mode 100644 index 67e9be45..00000000 --- a/lib/Solver/PCLoggingSolver.cpp +++ /dev/null @@ -1,68 +0,0 @@ -//===-- PCLoggingSolver.cpp -----------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "QueryLoggingSolver.h" - -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/Internal/Support/QueryLog.h" - -using namespace klee; - -/// - -class PCLoggingSolver : public QueryLoggingSolver { - -private : - ExprPPrinter *printer; - - virtual void printQuery(const Query& query, - const Query* falseQuery = 0, - const std::vector<const Array*>* objects = 0) { - - const ref<Expr>* evalExprsBegin = 0; - const ref<Expr>* evalExprsEnd = 0; - - if (0 != falseQuery) { - evalExprsBegin = &query.expr; - evalExprsEnd = &query.expr + 1; - } - - const Array* const *evalArraysBegin = 0; - const Array* const *evalArraysEnd = 0; - - if ((0 != objects) && (false == objects->empty())) { - evalArraysBegin = &((*objects)[0]); - evalArraysEnd = &((*objects)[0]) + objects->size(); - } - - const Query* q = (0 == falseQuery) ? &query : falseQuery; - - printer->printQuery(logBuffer, q->constraints, q->expr, - evalExprsBegin, evalExprsEnd, - evalArraysBegin, evalArraysEnd); - } - -public: - PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) - : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), - printer(ExprPPrinter::create(logBuffer)) { - } - - virtual ~PCLoggingSolver() { - delete printer; - } -}; - -/// - -Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path, - int minQueryTimeToLog) { - return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog)); -} |