diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-11 17:26:20 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-13 10:09:06 +0000 |
commit | 50f435267cf3a63a55971bd56d1c34058103c37b (patch) | |
tree | 70b31d96576a51ae5f8a654be143f7a1f6799add /tools | |
parent | 562d5516944325e96c91af623197b7d9cd0d9194 (diff) | |
download | klee-50f435267cf3a63a55971bd56d1c34058103c37b.tar.gz |
Renamed --no-output to --write-no-tests and placed it in the test case category (with --write-cov, --write-cvcs etc.)
Diffstat (limited to 'tools')
-rw-r--r-- | tools/klee/main.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 033ff5b1..cc9d0943 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -83,6 +83,12 @@ namespace { "These options select the files to generate for each test case."); cl::opt<bool> + WriteNone("write-no-tests", + cl::init(false), + cl::desc("Do not generate any test files (default=false)"), + cl::cat(TestCaseCat)); + + cl::opt<bool> WriteCVCs("write-cvcs", cl::desc("Write .cvc files for each test case (default=false)"), cl::cat(TestCaseCat)); @@ -205,12 +211,6 @@ namespace { cl::init(true), cl::cat(ChecksCat)); - - - cl::opt<bool> - NoOutput("no-output", - cl::desc("Don't generate test files (default=false).")); - cl::opt<bool> WarnAllExternals("warn-all-externals", cl::desc("Give initial warning for all externals (default=false).")); @@ -464,7 +464,7 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id) { void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix) { - if (!NoOutput) { + if (!WriteNone) { std::vector< std::pair<std::string, std::vector<unsigned char> > > out; bool success = m_interpreter->getSymbolicSolution(state, out); @@ -540,7 +540,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, *f << constraints; } - if(WriteSMT2s) { + if (WriteSMT2s) { std::string constraints; m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); auto f = openTestFile("smt2", id); @@ -582,7 +582,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (f) *f << "Time to generate test case: " << elapsed_time << '\n'; } - } + } // if (!WriteNone) if (errorMessage && OptExitOnError) { m_interpreter->prepareForEarlyExit(); |