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:¶

--no-assertions

ignore user assertions

--no-assumptions

ignore user assumptions

--cover CC

Add instrumentation as used with jbmc(1) for creating 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

--verbosity n

verbosity level

--timestamp [monotonic|wall]

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