Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- $klee --help
- OVERVIEW: klee
- USAGE: klee [options] <input bytecode> <program arguments>...
- OPTIONS:
- -all-external-warnings -
- -allow-external-sym-calls -
- -allow-seed-extension - Allow extra (unbound) values to become symbolic during seeding.
- -allow-seed-truncation - Allow smaller buffers than in seeds.
- -always-output-seeds -
- -asm-verbose - Add comments to directives.
- -batch-instructions=<uint> - Number of instructions to batch when using --use-batching-search
- -batch-time=<number> - Amount of time to batch when using --use-batching-search
- -cex-cache-exp -
- -cex-cache-try-all - try substituting all counterexamples before asking STP
- -check-div-zero - Inject checks for division-by-zero
- -code-model - Choose code model
- =default - Target default code model
- =small - Small code model
- =kernel - Kernel code model
- =medium - Medium code model
- =large - Large code model
- -const-array-opt - Enable various optimizations involving all-constant arrays.
- -debug-cex-cache-check-binding -
- -debug-check-for-implied-values -
- -debug-log-merge -
- -debug-log-state-merge -
- -debug-print-escaping-functions - Print functions whose address is taken.
- -debug-print-instructions - Print instructions during execution.
- -debug-validate-solver -
- -disable-excess-fp-precision - Disable optimizations that may increase FP precision
- -disable-fp-elim - Disable frame pointer elimination optimization
- -disable-inlining - Do not run the inliner pass
- -disable-internalize - Do not mark all symbols as internal
- -disable-opt - Do not run any optimization passes
- -disable-post-RA-scheduler - Disable scheduling after register allocation
- -disable-spill-fusing - Disable fusing of spill code into instructions
- -dump-states-on-halt -
- -emit-all-errors - Generate tests cases for all errors (default=one per (error,instruction) pair)
- -enable-correct-eh-support - Make the -lowerinvoke pass insert expensive, but correct, EH code
- -enable-eh - Emit DWARF exception handling (default if target supports)
- -enable-finite-only-fp-math - Enable optimizations that assumes non- NaNs / +-Infs
- -enable-fp-mad - Enable less precise MAD instructions to be generated
- -enable-load-pre -
- -enable-sjlj-eh - Emit SJLJ exception handling (default if target supports)
- -enable-unsafe-fp-math - Enable optimizations that may decrease FP precision
- -environ=<string> - Parse environ from given file (in "env" format)
- -exit-on-error - Exit if errors occur
- -float-abi - Choose float ABI type
- =default - Target default float ABI type
- =soft - Soft float ABI (implied by -soft-float)
- =hard - Hard float ABI (uses FP registers)
- -help - Display available options (--help-hidden for more)
- -init-env - Create custom environment. Options that can be passed as arguments to the programs are: --sym-argv <max-len> --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options
- -internalize-public-api-file=<filename> - A file containing list of symbol names to preserve
- -internalize-public-api-list=<list> - A list of symbol names to preserve
- -istats-write-interval=<number> - Approximate number of seconds between istats writes (default: 10.0)
- -join-liveintervals - Coalesce copies (default=true)
- -libc - Choose libc version (none by default).
- =none - Don't link in a libc
- =klee - Link in klee libc
- =uclibc - Link in uclibc (adapted for klee)
- -limit-float-precision=<uint> - Generate low-precision inline sequences for some float libcalls
- -load=<pluginfilename> - Load the specified plugin
- -make-concrete-symbolic=<uint> - Rate at which to make concrete reads symbolic (0=off)
- -march=<string> - Architecture to generate assembly for (see --version)
- -mattr=<a1,+a2,-a3,...> - Target specific attributes (-mattr=help for details)
- -max-depth=<uint> - Only allow this many symbolic branches (0=off)
- -max-forks=<uint> - Only fork this many times (-1=off)
- -max-instruction-time=<number> - Only allow a single instruction to take this much time (default=0 (off))
- -max-memory=<uint> - Refuse to fork when more above this about of memory (in MB, 0=off)
- -max-memory-inhibit - Inhibit forking at memory cap (vs. random terminate)
- -max-static-cpfork-pct=<number> -
- -max-static-cpsolve-pct=<number> -
- -max-static-fork-pct=<number> -
- -max-static-solve-pct=<number> -
- -max-stp-time=<number> - Maximum amount of time for a single query (default=120s)
- -max-sym-array-size=<uint> -
- -max-time=<number> - Halt execution after the specified number of seconds (0=off)
- -mcpu=<cpu-name> - Target a specific cpu type (-mcpu=help for details)
- -merge-at-exit=<string> -
- -named-seed-matching - Use names to match symbolic objects to inputs.
- -no-externals - Do not allow external functin calls
- -no-output - Don't generate test files
- -no-prefer-cex -
- -no-truncate-source-lines - Don't truncate long lines in the output source
- -nozero-initialized-in-bss - Don't place zero-initialized symbols into bss section
- -only-output-states-covering-new -
- -only-replay-seeds - Discard states that do not have a seed.
- -only-seed - Stop execution after seeding is done without doing regular search.
- -optimize - Optimize before execution
- -output-dir=<string> - Directory to write results in (defaults to klee-out-N)
- -output-istats - Write instruction level statistics (in callgrind format)
- -output-module - Write the bitcode for the final transformed module
- -output-source - Write the assembly for the final transformed source
- -output-stats - Write running stats trace file
- -pc-all-const-widths -
- -pc-all-widths -
- -pc-multibyte-reads -
- -pc-prefix-width -
- -pc-width-as-arg -
- -posix-runtime - Link with POSIX runtime
- -pre-RA-sched - Instruction schedulers available (before register allocation):
- =fast - Fast suboptimal list scheduling
- =list-td - Top-down list scheduler
- =list-tdrr - Top-down register reduction list scheduling
- =list-burr - Bottom-up register reduction list scheduling
- =default - Best scheduler for the target
- -print-machineinstrs - Print generated machine code
- -randomize-fork -
- -read-args=<string> - File to read arguments from (one arg per line)
- -realign-stack - Realign stack if needed
- -regalloc - Register allocator to use: (default = linearscan)
- =linearscan - linear scan register allocator
- -relocation-model - Choose relocation model
- =default - Target default relocation model
- =static - Non-relocatable code
- =pic - Fully relocatable, position independent code
- =dynamic-no-pic - Relocatable external references, non-relocatable code
- -replay-keep-symbolic - Replay the test cases only by assertingthe bytes, not necessarily making them concrete.
- -replay-out=<out file> - Specify an out file to replay
- -replay-out-dir=<output directory> - Specify a directory to replay .out files from
- -replay-path=<path file> - Specify a path file to replay
- -rewriter - Rewriter to use: (default: local)
- =local - local rewriter
- =trivial - trivial rewriter
- -run-in=<string> - Change to the given directory prior to executing
- -schedule-livein-copies - Schedule copies of livein registers
- -schedule-spills - Schedule spill code
- -seed-out=<string> -
- -seed-out-dir=<string> -
- -seed-time=<number> - Amount of time to dedicate to seeds, before normal search (default=0 (off))
- -shrink-wrap - Shrink wrap callee-saved register spills/restores
- -simplify-sym-indices -
- -soft-float - Generate software floating point library calls
- -stack-alignment=<uint> - Override default stack alignment
- -stack-protector-buffer-size=<uint> - Lower bound for a buffer to be considered for stack protection
- -stats - Enable statistics output from program
- -stats-write-interval=<number> - Approximate number of seconds between stats writes (default: 1.0)
- -stop-after-n-instructions=<uint> - Stop execution after specified number of instructions (0=off)
- -stop-after-n-tests=<uint> - Stop execution after generating the given number of tests. Extra tests corresponding to partially explored paths will also be dumped.
- -stp-optimize-divides - Optimize constant divides into add/shift/multiplies before passing to STP
- -strip-all - Strip all symbol info from executable
- -strip-debug - Strip debugger symbol info from executable
- -suppress-external-warnings -
- -switch-type - Select the implementation of switch
- =simple - lower to ordered branches
- =llvm - lower using LLVM
- =internal - execute switch internally
- -tailcallopt - Turn on tail call optimization.
- -time-passes - Time each pass, printing elapsed time for each on exit
- -track-instruction-time - Enable tracking of time for individual instructions
- -uncovered-update-interval=<number> -
- -unwind-tables - Generate unwinding tables for all functions
- -use-asm-addresses -
- -use-batching-search - Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time
- -use-bump-merge - Enable support for klee_merge() (extra experimental)
- -use-cache - Use validity caching
- -use-call-paths - Enable calltree tracking for instruction level statistics
- -use-cex-cache - Use counterexample caching
- -use-constant-arrays -
- -use-construct-hash - Use hash-consing during STP query construction.
- -use-fast-cex-solver -
- -use-forked-stp - Run STP in forked process
- -use-independent-solver - Use constraint independence
- -use-interleaved-MD2U-NURS -
- -use-interleaved-NURS -
- -use-interleaved-RS -
- -use-interleaved-covnew-NURS -
- -use-interleaved-cpicnt-NURS -
- -use-interleaved-icnt-NURS -
- -use-interleaved-query-cost-NURS -
- -use-iterative-deepening-time-search - (experimental)
- -use-merge - Enable support for klee_merge() (experimental)
- -use-non-uniform-random-search -
- -use-query-pc-log -
- -use-random-path -
- -use-random-search -
- -use-stp-query-pc-log -
- -use-visitor-hash - Use hash-consing during expr visitation.
- -verify-dom-info - Verify dominator info (time consuming)
- -verify-each - Verify intermediate results of all passes
- -version - Display the version of this program
- -warn-all-externals - Give initial warning for all externals.
- -watchdog - Use a watchdog process to enforce --max-time.
- -weight-type - Set the weight type for --use-non-uniform-random-search
- =none - use (2^depth)
- =icnt - use current pc exec count
- =cpicnt - use current pc exec count
- =query-cost - use query cost
- =md2u - use min dist to uncovered
- =covnew - use min dist to uncovered + coveringNew flag
- -write-cov - Write coverage information for each test case
- -write-cvcs - Write .cvc files for each test case
- -write-paths - Write .path files for each test case
- -write-pcs - Write .pc files for each test case
- -write-sym-paths - Write .sym.path files for each test case
- -write-test-info - Write additional test case information
- -x86-asm-syntax - Choose style of code to emit from X86 backend:
- =att - Emit AT&T-style assembly
- =intel - Emit Intel-style assembly
- -zero-seed-extension
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
