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
COPYRIGHT
2016, Daniel Kroening, Peter Schrammel