Your company here — click to reach over 10,000 unique daily visitors

goto-diff - Man Page

Syntactic diff of goto binaries


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

show help

goto-diff old new

goto binaries to be compared



Diff options


show loaded goto program


list loaded goto functions


show the properties, but don't run analysis


show the loops in the programs

-u | --unified

output unified diff

--change-impact |

--forward-impact |


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


output dependencies in compact mode

Program instrumentation options


enable array bounds checks


enable pointer checks


enable memory leak checks


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


enable division by zero checks


enable signed arithmetic over- and underflow checks


enable arithmetic over- and underflow checks


enable pointer arithmetic over- and underflow checks


check whether values can be represented after type cast


check shift greater than bit-width


check floating-point for +/-Inf


check floating-point for NaN


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


checks that all pointers in pointer primitives are valid or null


include checks that are trivially true

--error-label label

check that label is unreachable


ignore assertions in built-in library


ignore user assertions


ignore user assumptions


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


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


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

Other options


show version and exit


use JSON-formatted output


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.


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


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

See Also

cbmc(1), goto-analyzer(1)


June 2022 jdiff-5.59.0