oracular (1) goto-diff.1.gz

Provided by: cbmc_6.1.1-2_amd64 bug

NAME
       goto-diff - Syntactic diff of goto binaries


SYNOPSIS
       goto-diff [-?] [-h] [--help]
              show help

       goto-diff old new
              goto binaries to be compared


DESCRIPTION
OPTIONS
   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:
       --bounds-check
              enable array bounds checks

       --pointer-check
              enable pointer checks

       --memory-leak-check
              enable memory leak checks

       --memory-cleanup-check
              Enable  memory  cleanup  checks:  assert that all dynamically allocated memory is explicitly freed
              before terminating the program.

       --div-by-zero-check
              enable division by zero checks for integer division

       --float-div-by-zero-check
              enable division by zero checks for floating-point division

       --signed-overflow-check
              enable 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

       --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

       --retain-trivial-checks
              include checks that are trivially true

       --error-label label
              check that 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 n
              verbosity level

       --timestamp [monotonic|wall]
              Print microsecond-precision timestamps.  monotonic: stamps increase monotonically.  wall: ISO-8601
              wall clock timestamps.


ENVIRONMENT
       All tools honor the TMPDIR environment variable when generating temporary files and directories.


BUGS
       If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues


SEE ALSO
       cbmc(1), goto-analyzer(1)


       2016, Daniel Kroening, Peter Schrammel