GOTO-DIFF(1) User Commands GOTO-DIFF(1)

# [NAME](#NAME)

goto-diff - Syntactic diff of goto binaries

# [SYNOPSIS](#SYNOPSIS)

[**goto-diff \[-?\] \[-h\] \[--help\]**](#goto)

show help

[**goto-diff old new**](#goto~2)

goto binaries to be compared

# [DESCRIPTION](#DESCRIPTION)

# [OPTIONS](#OPTIONS)

## [Diff options:](#Diff_options:)

[**--show-goto-functions**](#show)

show loaded goto program

[**--list-goto-functions**](#list)

list loaded goto functions

[**--show-properties**](#show~2)

show the properties, but don't run analysis

[**--show-loops**](#show~3)

show the loops in the programs

[**-u** | **--unified**](#u)

output unified diff

**--change-impact** |

**--forward-impact** |

[**--backward-impact**](#backward)

output unified diff with forward&backward/forward/backward dependencies

[**--compact-output**](#compact)

output dependencies in compact mode

## [Program instrumentation options:](#Program_instrumentation_options:)

[**--bounds-check**](#bounds)

enable array bounds checks

[**--pointer-check**](#pointer)

enable pointer checks

[**--memory-leak-check**](#memory)

enable memory leak checks

[**--memory-cleanup-check**](#memory~2)

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

[**--div-by-zero-check**](#div)

enable division by zero checks for integer division

[**--float-div-by-zero-check**](#float)

enable division by zero checks for floating-point division

[**--signed-overflow-check**](#signed)

enable signed arithmetic over- and underflow checks

[**--unsigned-overflow-check**](#unsigned)

enable arithmetic over- and underflow checks

[**--pointer-overflow-check**](#pointer~2)

enable pointer arithmetic over- and underflow checks

[**--conversion-check**](#conversion)

check whether values can be represented after type cast

[**--undefined-shift-check**](#undefined)

check shift greater than bit-width

[**--float-overflow-check**](#float~2)

check floating-point for +/-Inf

[**--nan-check**](#nan)

check floating-point for NaN

[**--enum-range-check**](#enum)

checks that all enum type expressions have values in the enum range

[**--pointer-primitive-check**](#pointer~3)

checks that all pointers in pointer primitives are valid or null

[**--retain-trivial-checks**](#retain)

include checks that are trivially true

[**--error-label** label](#error)

check that label is unreachable

[**--no-built-in-assertions**](#no)

ignore assertions in built-in library

[**--no-assertions**](#no~2)

ignore user assertions

[**--no-assumptions**](#no~3)

ignore user assumptions

[**--assert-to-assume**](#assert)

convert user assertions to assumptions

[**--cover** CC](#cover)

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**](#cover~2)

do not stop coverage checking at failed assertions (this is the default for **--cover** assertions)

[**--show-test-suite**](#show~4)

print test suite for coverage criterion (requires **--cover**)

## [Other options:](#Other_options:)

[**--version**](#version)

show version and exit

[**--json-ui**](#json)

use JSON-formatted output

[**--flush**](#flush)

flush every line of output

[**--verbosity** *n*](#verbosity)

verbosity level

[**--timestamp** \[**monotonic**|**wall**\]](#timestamp)

Print microsecond-precision timestamps. **monotonic**: stamps increase monotonically. **wall**: ISO-8601 wall clock timestamps.

# [ENVIRONMENT](#ENVIRONMENT)

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

# [BUGS](#BUGS)

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

# [SEE ALSO](#SEE_ALSO)

[**cbmc**(1)](/man/os/cbmc/cbmc.1), [**goto-analyzer**(1)](/man/os/cbmc/goto-analyzer.1)

# [COPYRIGHT](#COPYRIGHT)

2016, Daniel Kroening, Peter Schrammel

June 2022 jdiff-5.59.0

---

Document: goto-diff(1) from cbmc 6.11.0-r0 (Chainguard OS)