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.