/usr/bin/goto-analyzer

* *     GOTO-ANALYZER 6.11.0 (cbmc-6.11.0-dirty) 64-bit     * *
* *                 Copyright (C) 2017-2018                 * *
* *                Daniel Kroening, Diffblue                * *
* *                  kroening@kroening.com                  * *

Usage:                       Purpose:

 goto-analyzer [-?|-h|--help]  show this help
 goto-analyzer file.c...      source file names

Task options:
 --show                       display the abstract states on the goto program
 --show-on-source             display the abstract states on the source
 --verify                     use the abstract domains to check assertions
 --simplify file_name         use the abstract domains to simplify the program
 --no-simplify-slicing        do not remove instructions from which no property
                              can be reached (use with --simplify)
 --unreachable-instructions   list dead code
 --unreachable-functions      list functions unreachable from the entry point
 --reachable-functions        list functions reachable from the entry point

Abstract interpreter options:
 --legacy-ait                 recursion for function and one domain per location
 --recursive-interprocedural  use recursion to handle interprocedural reasoning
 --three-way-merge            use VSD's three-way merge on return from function
                              call
 --legacy-concurrent          legacy-ait with an extended fixed-point for
                              concurrency
 --location-sensitive         use location-sensitive abstract interpreter

History options:
 --ahistorical                the most basic history, tracks locations only
 --call-stack n               track the calling location stack for each
                              function limiting to at most n recursive loops, 0
                              to disable
 --loop-unwind n              track the number of loop iterations within a
                              function limited to n histories per location, 0
                              is unlimited
 --branching n                track the forwards jumps (if, switch, etc.)
                              within a function limited to n histories per
                              location, 0 is unlimited
 --loop-unwind-and-branching n  track all local control flow limited to n
                              histories per location, 0 is unlimited

Domain options:
 --constants                  a constant for each variable if possible
 --intervals                  an interval for each variable
 --non-null                   tracks which pointers are non-null
 --dependence-graph           data and control dependencies between instructions
 --vsd, --variable-sensitivity  a configurable non-relational domain
 --dependence-graph-vs        dependencies between instructions using VSD

Variable sensitivity domain (VSD) options:
 --vsd-values [constants|intervals|set-of-constants]  value tracking
 --vsd-structs [top-bottom|every-field]  struct field sensitive analysis
 --vsd-arrays [top-bottom|smash|up-to-n-elements|every-element]  array entry
                              sensitive analysis
 --vsd-array-max-elements N   set the n in --vsd-arrays up-to-n-elements
                              (defaults to 10 if not given)
 --vsd-pointers [top-bottom|constants|value-set]  pointer sensitive analysis
 --vsd-unions [top-bottom]    union sensitive analysis
 --vsd-data-dependencies      track data dependencies
 --vsd-liveness               track variable liveness
 --vsd-flow-insensitive       disables flow sensitivity

Storage options:
 --one-domain-per-location    stores a domain for each location reached
 --one-domain-per-history     stores a domain for each history object created

Output options:
 --text file_name             output results in plain text to given file
 --json file_name             output results in JSON format to given file
 --xml file_name              output results in XML format to given file
 --dot file_name              output results in DOT format to given file

Specific analyses:
 --taint file_name            perform taint analysis using rules in given file
 --show-taint                 print taint analysis results on stdout
 --show-local-bitvector       perform procedure-local bitvector analysis
 --show-local-may-alias       perform procedure-local may alias analysis

C/C++ frontend options:
 -I path                      set include path (C/C++)
 --include file               set include file (C/C++)
 -D macro                     define preprocessor macro (C/C++)
 --c89, --c99, --c11,
 --c17, --c23                 set C language standard (default: c11)
 --cpp98, --cpp03, --cpp11    set C++ language standard (default: cpp98)
 --unsigned-char              make "char" unsigned by default
 --round-to-nearest, --round-to-even  rounding towards nearest even (default)
 --round-to-plus-inf          rounding towards plus infinity
 --round-to-minus-inf         rounding towards minus infinity
 --round-to-zero              rounding towards zero
 --no-library                 disable built-in abstract C library
 --function name              set main function name

Platform options:
 --arch arch_name             set architecture (default: x86_64) to one of:
                              alpha, arm, arm64, armel, armhf, hppa, i386, ia64
                              , mips, mips64, mips64el, mipsel, mipsn32,
                              mipsn32el, powerpc, ppc64, ppc64le, riscv64, s390
                              , s390x, sh4, sparc, sparc64, v850, x32, x86_64,
                              or none
 --os os_name                 set operating system (default: linux) to one of:
                              freebsd, linux, macos, netbsd, openbsd, solaris,
                              hurd, or windows
 --i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64  set
                              architecture and operating system
 --LP64, --ILP64, --LLP64, --ILP32, --LP32  set width of int, long and
                              pointers, but don't override default architecture
                              and operating system
 --16, --32, --64             equivalent to --LP32, --ILP32, --LP64 (on
                              Windows: --LLP64)
 --little-endian              allow little-endian word-byte conversions
 --big-endian                 allow big-endian word-byte conversions
 --gcc                        use GCC as preprocessor

Program representations:
 --show-parse-tree            show parse tree
 --show-symbol-table          show loaded symbol table
 --show-goto-functions        show loaded goto program
 --list-goto-functions        list loaded goto functions
 --show-properties            show the properties, but don't run analysis

Program instrumentation options:
 --property id                enable selected properties only
 --no-standard-checks         disable default checks (more information in
                              manpage)
 --bounds-check               enable array bounds checks (default on)
 --no-bounds-check            disable array bounds checks
 --pointer-check              enable pointer checks (default on)
 --no-pointer-check           disable pointer checks
 --memory-leak-check          enable memory leak checks
 --memory-cleanup-check       enable memory cleanup checks
 --div-by-zero-check          enable division by zero checks on integers
                              (default on)
 --float-div-by-zero-check    enable division by zero checks on floating-point
                              numbers (default off)
 --no-div-by-zero-check       disable division by zero checks
 --signed-overflow-check      enable signed arithmetic over- and underflow
                              checks (default on)
 --no-signed-overflow-check   disable signed arithmetic over- and underflow
                              checks
 --unsigned-overflow-check    enable arithmetic over- and underflow checks
 --pointer-overflow-check     enable pointer arithmetic over- and underflow
                              checks
 --conversion-check           check whether values can be represented after
                              type cast
 --undefined-shift-check      check shift greater than bit-width (default on)
 --no-undefined-shift-check   disable check for shift greater than bit-width
 --float-overflow-check       check floating-point for +/-Inf
 --nan-check                  check floating-point for NaN
 --enum-range-check           checks that all enum type expressions have values
                              in the enum range
 --pointer-primitive-check    checks that all pointers in pointer primitives
                              are valid or null (default on)
 --no-pointer-primitive-check  disable checks that all pointers in pointer
                              primitives are valid or null
 --retain-trivial-checks      include checks that are trivially true
 --error-label label          check that label label is unreachable
 --no-built-in-assertions     ignore assertions in built-in library
 --no-assertions              ignore user assertions
 --no-assumptions             ignore user assumptions
 --assert-to-assume           convert user assertions to assumptions
 --malloc-may-fail            allow malloc calls to return a null pointer
 --no-malloc-may-fail         disable potential malloc failure
 --malloc-fail-assert         set malloc failure mode to assert-then-assume
 --malloc-fail-null           set malloc failure mode to return null
 --string-abstraction         track C string lengths and zero-termination
 --dfcc-debug-lib             enable debug assertions in the cprover contracts
                              library
 --dfcc-simple-invalid-pointer-model  use simplified invalid pointer model in
                              the cprover contracts library (faster, unsound)

Other options:
 --validate-goto-model        enable additional well-formedness checks on the
                              goto program
 --validate-ssa-equation      enable additional well-formedness checks on the
                              SSA representation
 --version                    show version and exit
 --flush                      flush every line of output
 --verbosity #                verbosity level
 --timestamp [monotonic|wall]  print microsecond-precision timestamps. monotonic
                              : stamps increase monotonically. wall: ISO-8601
                              wall clock timestamps.