Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Klee options

a guest Oct 7th, 2010 802 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  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
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top