aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2018-12-18 15:17:28 +0000
committerMartinNowack <martin.nowack@gmail.com>2018-12-19 21:26:48 +0000
commitb7b53fa5a7dbeb906fff9b117b76944fd6de27a2 (patch)
tree08f723a12c493e3aac50e52e9c98ecb681e133b9
parent6a8ec2bd4d9b1c2c70408d529a50c8c1c3d041ef (diff)
downloadklee-b7b53fa5a7dbeb906fff9b117b76944fd6de27a2.tar.gz
Added checks option category, moved --optimize to starting category, renamed original --run-in option to --running-dir
-rw-r--r--test/Runtime/POSIX/DirConsistency.c4
-rw-r--r--test/Runtime/POSIX/DirSeek.c6
-rw-r--r--tools/klee/main.cpp53
3 files changed, 37 insertions, 26 deletions
diff --git a/test/Runtime/POSIX/DirConsistency.c b/test/Runtime/POSIX/DirConsistency.c
index 43216d54..7b1d4a74 100644
--- a/test/Runtime/POSIX/DirConsistency.c
+++ b/test/Runtime/POSIX/DirConsistency.c
@@ -1,11 +1,11 @@
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
-// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
+// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
// RUN: %llvmgcc -D_FILE_OFFSET_BITS=64 %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
-// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
+// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
// RUN: sort %t1.log %t2.log | uniq -c > %t3.log
// RUN: grep -q "4 COUNT" %t3.log
diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c
index 449714b9..e7be5503 100644
--- a/test/Runtime/POSIX/DirSeek.c
+++ b/test/Runtime/POSIX/DirSeek.c
@@ -1,13 +1,13 @@
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -g -o %t2.bc
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
-// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 2 2
+// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 2 2
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
-// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2
+// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
-// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2 --sym-stdin 2
+// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2 --sym-stdin 2
// For this test really to work as intended it needs to be run in a
// directory large enough to cause uclibc to do multiple getdents
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index af97b759..a5130429 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -133,14 +133,26 @@ namespace {
cl::opt<std::string>
RunInDir("run-in-dir",
- cl::desc("Change to the given directory prior to executing"),
+ cl::desc("Change to the given directory before starting execution"),
cl::cat(StartCat));
+
+ cl::opt<std::string>
+ OutputDir("output-dir",
+ cl::desc("Directory in which to write results (default=klee-out-<N>)"),
+ cl::init(""),
+ cl::cat(StartCat));
cl::opt<std::string>
Environ("environ",
cl::desc("Parse environment from given file (in \"env\" format)"),
cl::cat(StartCat));
+ cl::opt<bool>
+ OptimizeModule("optimize",
+ cl::desc("Optimize the code before execution"),
+ cl::init(false),
+ cl::cat(StartCat));
+
/*** Linking options ***/
@@ -178,6 +190,25 @@ namespace {
cl::cat(LinkCat));
+ /*** Checks options ***/
+
+ cl::OptionCategory ChecksCat("Checks options",
+ "These options control some of the checks being done by KLEE.");
+
+ cl::opt<bool>
+ CheckDivZero("check-div-zero",
+ cl::desc("Inject checks for division-by-zero (default=true)"),
+ cl::init(true),
+ cl::cat(ChecksCat));
+
+ cl::opt<bool>
+ CheckOvershift("check-overshift",
+ cl::desc("Inject checks for overshift (default=true)"),
+ cl::init(true),
+ cl::cat(ChecksCat));
+
+
+
cl::opt<bool>
NoOutput("no-output",
cl::desc("Don't generate test files"));
@@ -191,26 +222,6 @@ namespace {
cl::desc("Exit if errors occur"));
cl::opt<bool>
- OptimizeModule("optimize",
- cl::desc("Optimize before execution"),
- cl::init(false));
-
- cl::opt<bool>
- CheckDivZero("check-div-zero",
- cl::desc("Inject checks for division-by-zero"),
- cl::init(true));
-
- cl::opt<bool>
- CheckOvershift("check-overshift",
- cl::desc("Inject checks for overshift"),
- cl::init(true));
-
- cl::opt<std::string>
- OutputDir("output-dir",
- cl::desc("Directory to write results in (defaults to klee-out-N)"),
- cl::init(""));
-
- cl::opt<bool>
ReplayKeepSymbolic("replay-keep-symbolic",
cl::desc("Replay the test cases only by asserting "
"the bytes, not necessarily making them concrete."));