---
name: "goto-diff"
section: "1"
platform: "linux"
package: "cbmc"
version: "6.6.0-4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/goto-diff"
---

# goto-diff(1)

Syntactic diff of goto binaries

## 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)](/cbmc/1.md), [**goto-analyzer**(1)](/goto-analyzer/1.md)

## COPYRIGHT

2016, Daniel Kroening, Peter Schrammel