SHARE
TWEET

Klee options

a guest Oct 7th, 2010 688 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. $klee --help
  2. OVERVIEW:  klee
  3.  
  4. USAGE: klee [options] <input bytecode> <program arguments>...
  5.  
  6. OPTIONS:
  7.   -all-external-warnings                  -
  8.   -allow-external-sym-calls               -
  9.   -allow-seed-extension                   - Allow extra (unbound) values to become symbolic during seeding.
  10.   -allow-seed-truncation                  - Allow smaller buffers than in seeds.
  11.   -always-output-seeds                    -
  12.   -asm-verbose                            - Add comments to directives.
  13.   -batch-instructions=<uint>              - Number of instructions to batch when using --use-batching-search
  14.   -batch-time=<number>                    - Amount of time to batch when using --use-batching-search
  15.   -cex-cache-exp                          -
  16.   -cex-cache-try-all                      - try substituting all counterexamples before asking STP
  17.   -check-div-zero                         - Inject checks for division-by-zero
  18.   -code-model                             - Choose code model
  19.     =default                              -   Target default code model
  20.     =small                                -   Small code model
  21.     =kernel                               -   Kernel code model
  22.     =medium                               -   Medium code model
  23.     =large                                -   Large code model
  24.   -const-array-opt                        - Enable various optimizations involving all-constant arrays.
  25.   -debug-cex-cache-check-binding          -
  26.   -debug-check-for-implied-values         -
  27.   -debug-log-merge                        -
  28.   -debug-log-state-merge                  -
  29.   -debug-print-escaping-functions         - Print functions whose address is taken.
  30.   -debug-print-instructions               - Print instructions during execution.
  31.   -debug-validate-solver                  -
  32.   -disable-excess-fp-precision            - Disable optimizations that may increase FP precision
  33.   -disable-fp-elim                        - Disable frame pointer elimination optimization
  34.   -disable-inlining                       - Do not run the inliner pass
  35.   -disable-internalize                    - Do not mark all symbols as internal
  36.   -disable-opt                            - Do not run any optimization passes
  37.   -disable-post-RA-scheduler              - Disable scheduling after register allocation
  38.   -disable-spill-fusing                   - Disable fusing of spill code into instructions
  39.   -dump-states-on-halt                    -
  40.   -emit-all-errors                        - Generate tests cases for all errors (default=one per (error,instruction) pair)
  41.   -enable-correct-eh-support              - Make the -lowerinvoke pass insert expensive, but correct, EH code
  42.   -enable-eh                              - Emit DWARF exception handling (default if target supports)
  43.   -enable-finite-only-fp-math             - Enable optimizations that assumes non- NaNs / +-Infs
  44.   -enable-fp-mad                          - Enable less precise MAD instructions to be generated
  45.   -enable-load-pre                        -
  46.   -enable-sjlj-eh                         - Emit SJLJ exception handling (default if target supports)
  47.   -enable-unsafe-fp-math                  - Enable optimizations that may decrease FP precision
  48.   -environ=<string>                       - Parse environ from given file (in "env" format)
  49.   -exit-on-error                          - Exit if errors occur
  50.   -float-abi                              - Choose float ABI type
  51.     =default                              -   Target default float ABI type
  52.     =soft                                 -   Soft float ABI (implied by -soft-float)
  53.     =hard                                 -   Hard float ABI (uses FP registers)
  54.   -help                                   - Display available options (--help-hidden for more)
  55.   -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
  56.   -internalize-public-api-file=<filename> - A file containing list of symbol names to preserve
  57.   -internalize-public-api-list=<list>     - A list of symbol names to preserve
  58.   -istats-write-interval=<number>         - Approximate number of seconds between istats writes (default: 10.0)
  59.   -join-liveintervals                     - Coalesce copies (default=true)
  60.   -libc                                   - Choose libc version (none by default).
  61.     =none                                 -   Don't link in a libc
  62.    =klee                                 -   Link in klee libc
  63.    =uclibc                               -   Link in uclibc (adapted for klee)
  64.  -limit-float-precision=<uint>           - Generate low-precision inline sequences for some float libcalls
  65.  -load=<pluginfilename>                  - Load the specified plugin
  66.  -make-concrete-symbolic=<uint>          - Rate at which to make concrete reads symbolic (0=off)
  67.  -march=<string>                         - Architecture to generate assembly for (see --version)
  68.  -mattr=<a1,+a2,-a3,...>                 - Target specific attributes (-mattr=help for details)
  69.  -max-depth=<uint>                       - Only allow this many symbolic branches (0=off)
  70.  -max-forks=<uint>                       - Only fork this many times (-1=off)
  71.  -max-instruction-time=<number>          - Only allow a single instruction to take this much time (default=0 (off))
  72.  -max-memory=<uint>                      - Refuse to fork when more above this about of memory (in MB, 0=off)
  73.  -max-memory-inhibit                     - Inhibit forking at memory cap (vs. random terminate)
  74.  -max-static-cpfork-pct=<number>         -
  75.  -max-static-cpsolve-pct=<number>        -
  76.  -max-static-fork-pct=<number>           -
  77.  -max-static-solve-pct=<number>          -
  78.  -max-stp-time=<number>                  - Maximum amount of time for a single query (default=120s)
  79.  -max-sym-array-size=<uint>              -
  80.  -max-time=<number>                      - Halt execution after the specified number of seconds (0=off)
  81.  -mcpu=<cpu-name>                        - Target a specific cpu type (-mcpu=help for details)
  82.  -merge-at-exit=<string>                 -
  83.  -named-seed-matching                    - Use names to match symbolic objects to inputs.
  84.  -no-externals                           - Do not allow external functin calls
  85.  -no-output                              - Don't generate test files
  86.   -no-prefer-cex                          -
  87.   -no-truncate-source-lines               - Don't truncate long lines in the output source
  88.  -nozero-initialized-in-bss              - Don't place zero-initialized symbols into bss section
  89.   -only-output-states-covering-new        -
  90.   -only-replay-seeds                      - Discard states that do not have a seed.
  91.   -only-seed                              - Stop execution after seeding is done without doing regular search.
  92.   -optimize                               - Optimize before execution
  93.   -output-dir=<string>                    - Directory to write results in (defaults to klee-out-N)
  94.   -output-istats                          - Write instruction level statistics (in callgrind format)
  95.   -output-module                          - Write the bitcode for the final transformed module
  96.   -output-source                          - Write the assembly for the final transformed source
  97.   -output-stats                           - Write running stats trace file
  98.   -pc-all-const-widths                    -
  99.   -pc-all-widths                          -
  100.   -pc-multibyte-reads                     -
  101.   -pc-prefix-width                        -
  102.   -pc-width-as-arg                        -
  103.   -posix-runtime                          - Link with POSIX runtime
  104.   -pre-RA-sched                           - Instruction schedulers available (before register allocation):
  105.     =fast                                 -   Fast suboptimal list scheduling
  106.     =list-td                              -   Top-down list scheduler
  107.     =list-tdrr                            -   Top-down register reduction list scheduling
  108.     =list-burr                            -   Bottom-up register reduction list scheduling
  109.     =default                              -   Best scheduler for the target
  110.   -print-machineinstrs                    - Print generated machine code
  111.   -randomize-fork                         -
  112.   -read-args=<string>                     - File to read arguments from (one arg per line)
  113.   -realign-stack                          - Realign stack if needed
  114.   -regalloc                               - Register allocator to use: (default = linearscan)
  115.     =linearscan                           -   linear scan register allocator
  116.   -relocation-model                       - Choose relocation model
  117.     =default                              -   Target default relocation model
  118.     =static                               -   Non-relocatable code
  119.     =pic                                  -   Fully relocatable, position independent code
  120.     =dynamic-no-pic                       -   Relocatable external references, non-relocatable code
  121.   -replay-keep-symbolic                   - Replay the test cases only by assertingthe bytes, not necessarily making them concrete.
  122.   -replay-out=<out file>                  - Specify an out file to replay
  123.   -replay-out-dir=<output directory>      - Specify a directory to replay .out files from
  124.   -replay-path=<path file>                - Specify a path file to replay
  125.   -rewriter                               - Rewriter to use: (default: local)
  126.     =local                                -   local rewriter
  127.     =trivial                              -   trivial rewriter
  128.   -run-in=<string>                        - Change to the given directory prior to executing
  129.   -schedule-livein-copies                 - Schedule copies of livein registers
  130.   -schedule-spills                        - Schedule spill code
  131.   -seed-out=<string>                      -
  132.   -seed-out-dir=<string>                  -
  133.   -seed-time=<number>                     - Amount of time to dedicate to seeds, before normal search (default=0 (off))
  134.   -shrink-wrap                            - Shrink wrap callee-saved register spills/restores
  135.   -simplify-sym-indices                   -
  136.   -soft-float                             - Generate software floating point library calls
  137.   -stack-alignment=<uint>                 - Override default stack alignment
  138.   -stack-protector-buffer-size=<uint>     - Lower bound for a buffer to be considered for stack protection
  139.   -stats                                  - Enable statistics output from program
  140.   -stats-write-interval=<number>          - Approximate number of seconds between stats writes (default: 1.0)
  141.   -stop-after-n-instructions=<uint>       - Stop execution after specified number of instructions (0=off)
  142.   -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.
  143.   -stp-optimize-divides                   - Optimize constant divides into add/shift/multiplies before passing to STP
  144.   -strip-all                              - Strip all symbol info from executable
  145.   -strip-debug                            - Strip debugger symbol info from executable
  146.   -suppress-external-warnings             -
  147.   -switch-type                            - Select the implementation of switch
  148.     =simple                               -   lower to ordered branches
  149.     =llvm                                 -   lower using LLVM
  150.     =internal                             -   execute switch internally
  151.   -tailcallopt                            - Turn on tail call optimization.
  152.   -time-passes                            - Time each pass, printing elapsed time for each on exit
  153.   -track-instruction-time                 - Enable tracking of time for individual instructions
  154.   -uncovered-update-interval=<number>     -
  155.   -unwind-tables                          - Generate unwinding tables for all functions
  156.   -use-asm-addresses                      -
  157.   -use-batching-search                    - Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time
  158.   -use-bump-merge                         - Enable support for klee_merge() (extra experimental)
  159.   -use-cache                              - Use validity caching
  160.   -use-call-paths                         - Enable calltree tracking for instruction level statistics
  161.   -use-cex-cache                          - Use counterexample caching
  162.   -use-constant-arrays                    -
  163.   -use-construct-hash                     - Use hash-consing during STP query construction.
  164.   -use-fast-cex-solver                    -
  165.   -use-forked-stp                         - Run STP in forked process
  166.   -use-independent-solver                 - Use constraint independence
  167.   -use-interleaved-MD2U-NURS              -
  168.   -use-interleaved-NURS                   -
  169.   -use-interleaved-RS                     -
  170.   -use-interleaved-covnew-NURS            -
  171.   -use-interleaved-cpicnt-NURS            -
  172.   -use-interleaved-icnt-NURS              -
  173.   -use-interleaved-query-cost-NURS        -
  174.   -use-iterative-deepening-time-search    - (experimental)
  175.   -use-merge                              - Enable support for klee_merge() (experimental)
  176.   -use-non-uniform-random-search          -
  177.   -use-query-pc-log                       -
  178.   -use-random-path                        -
  179.   -use-random-search                      -
  180.   -use-stp-query-pc-log                   -
  181.   -use-visitor-hash                       - Use hash-consing during expr visitation.
  182.   -verify-dom-info                        - Verify dominator info (time consuming)
  183.   -verify-each                            - Verify intermediate results of all passes
  184.   -version                                - Display the version of this program
  185.   -warn-all-externals                     - Give initial warning for all externals.
  186.   -watchdog                               - Use a watchdog process to enforce --max-time.
  187.   -weight-type                            - Set the weight type for --use-non-uniform-random-search
  188.     =none                                 -   use (2^depth)
  189.     =icnt                                 -   use current pc exec count
  190.     =cpicnt                               -   use current pc exec count
  191.     =query-cost                           -   use query cost
  192.     =md2u                                 -   use min dist to uncovered
  193.     =covnew                               -   use min dist to uncovered + coveringNew flag
  194.   -write-cov                              - Write coverage information for each test case
  195.   -write-cvcs                             - Write .cvc files for each test case
  196.   -write-paths                            - Write .path files for each test case
  197.   -write-pcs                              - Write .pc files for each test case
  198.   -write-sym-paths                        - Write .sym.path files for each test case
  199.   -write-test-info                        - Write additional test case information
  200.   -x86-asm-syntax                         - Choose style of code to emit from X86 backend:
  201.     =att                                  -   Emit AT&T-style assembly
  202.     =intel                                -   Emit Intel-style assembly
  203.   -zero-seed-extension
RAW Paste Data
Want to get better at Bash?
Learn to code Bash in 2017
Pastebin PRO Summer Special!
Get 40% OFF on Pastebin PRO accounts!
Top