diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-12-18 15:17:28 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-12-19 21:26:48 +0000 |
commit | b7b53fa5a7dbeb906fff9b117b76944fd6de27a2 (patch) | |
tree | 08f723a12c493e3aac50e52e9c98ecb681e133b9 | |
parent | 6a8ec2bd4d9b1c2c70408d529a50c8c1c3d041ef (diff) | |
download | klee-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.c | 4 | ||||
-rw-r--r-- | test/Runtime/POSIX/DirSeek.c | 6 | ||||
-rw-r--r-- | tools/klee/main.cpp | 53 |
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.")); |