diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/kleaver/main.cpp | 4 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index a937d761..3fde0abf 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -224,8 +224,8 @@ static bool EvaluateInputAST(const char *Filename, Solver *S = constructSolverChain(coreSolver, getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); + getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME)); unsigned Index = 0; for (std::vector<Decl*>::iterator it = Decls.begin(), diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index ee20f5ea..c4eaa30c 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -107,8 +107,8 @@ namespace { cl::desc("Write .cvc files for each test case")); cl::opt<bool> - WritePCs("write-pcs", - cl::desc("Write .pc files for each test case")); + WriteKQueries("write-kqueries", + cl::desc("Write .kquery files for each test case")); cl::opt<bool> WriteSMT2s("write-smt2s", @@ -416,7 +416,7 @@ llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix, } -/* Outputs all files (.ktest, .pc, .cov etc.) describing a test case */ +/* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */ void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix) { @@ -482,10 +482,10 @@ void KleeHandler::processTestCase(const ExecutionState &state, delete f; } - if (errorMessage || WritePCs) { + if (errorMessage || WriteKQueries) { std::string constraints; m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY); - llvm::raw_ostream *f = openTestFile("pc", id); + llvm::raw_ostream *f = openTestFile("kquery", id); *f << constraints; delete f; } |