* *       GOTO_DIFF 6.11.0 (cbmc-6.11.0-dirty) 64-bit       * *
* *                    Copyright (C) 2016                   * *
* *             Daniel Kroening, Peter Schrammel            * *
* *                  kroening@kroening.com                  * *

Usage:                       Purpose:

 goto-diff [-?] [-h] [--help]  show this help
 goto-diff old new            compare two goto binaries

Diff options:
 --show-goto-functions        show loaded goto program
 --list-goto-functions        list loaded goto functions
 --show-properties            show the properties, but don't run analysis
 --show-loops                 show the loops in the programs
 -u, --unified                output unified diff
 --change-impact, --forward-impact, --backward-impact  output unified diff with
                              forward&backward/forward/backward dependencies
 --compact-output             output dependencies in compact mode

Program instrumentation options:
 --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
 --cover CC                   create test-suite with coverage criterion CC,
                              where CC is one of assertion[s], assume[s], branch
                              [es], condition[s], cover, decision[s], location[s
                              ], or mcdc
 --cover-failed-assertions    do not stop coverage checking at failed
                              assertions (this is the default for --cover
                              assertions)
 --show-test-suite            print test suite for coverage criterion (requires
                              --cover)

Other options:
 --version                    show version and exit
 --json-ui                    use JSON-formatted output
 --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.