about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-11 17:26:20 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-13 10:09:06 +0000
commit50f435267cf3a63a55971bd56d1c34058103c37b (patch)
tree70b31d96576a51ae5f8a654be143f7a1f6799add /tools
parent562d5516944325e96c91af623197b7d9cd0d9194 (diff)
downloadklee-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.cpp18
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();