From b7b53fa5a7dbeb906fff9b117b76944fd6de27a2 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 18 Dec 2018 15:17:28 +0000 Subject: Added checks option category, moved --optimize to starting category, renamed original --run-in option to --running-dir --- tools/klee/main.cpp | 53 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 32 insertions(+), 21 deletions(-) (limited to 'tools') 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 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 + OutputDir("output-dir", + cl::desc("Directory in which to write results (default=klee-out-)"), + cl::init(""), + cl::cat(StartCat)); cl::opt Environ("environ", cl::desc("Parse environment from given file (in \"env\" format)"), cl::cat(StartCat)); + cl::opt + 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 + CheckDivZero("check-div-zero", + cl::desc("Inject checks for division-by-zero (default=true)"), + cl::init(true), + cl::cat(ChecksCat)); + + cl::opt + CheckOvershift("check-overshift", + cl::desc("Inject checks for overshift (default=true)"), + cl::init(true), + cl::cat(ChecksCat)); + + + cl::opt NoOutput("no-output", cl::desc("Don't generate test files")); @@ -190,26 +221,6 @@ namespace { OptExitOnError("exit-on-error", cl::desc("Exit if errors occur")); - cl::opt - OptimizeModule("optimize", - cl::desc("Optimize before execution"), - cl::init(false)); - - cl::opt - CheckDivZero("check-div-zero", - cl::desc("Inject checks for division-by-zero"), - cl::init(true)); - - cl::opt - CheckOvershift("check-overshift", - cl::desc("Inject checks for overshift"), - cl::init(true)); - - cl::opt - OutputDir("output-dir", - cl::desc("Directory to write results in (defaults to klee-out-N)"), - cl::init("")); - cl::opt ReplayKeepSymbolic("replay-keep-symbolic", cl::desc("Replay the test cases only by asserting " -- cgit 1.4.1