Klee options

$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

 -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