cbmc(1) on Linux
The text ef3ad1a74f0c, as Debian 10 (Buster), Debian 9 (Stretch) shipped it.
Bounded Model Checker for C/C++ and Java programs
Flags it lists
-
--16 -
--32 -
--64 -
--ILP32 -
--ILP64 -
--LLP64 -
--LP32 -
--LP64 -
--all-properties -
--arch -
--arrays-uf-always -
--arrays-uf-never -
--beautify-greedy -
--big-endian -
--boolector -
--bounds-check -
--cover-assertions -
--cvc -
--depth -
--dimacs -
--div-by-zero-check -
--dump-c -
--error-label -
--function -
--isr -
--little-endian -
--mathsat -
--mmio -
--nan-check -
--no-arch -
--no-assertions -
--no-assumptions -
--no-library -
--no-pretty-names -
--no-unwinding-assertions -
--nondet-static -
--nondet-volatile -
--os -
--outfile -
--pointer-check -
--preprocess -
--program-only -
--property -
--refine -
--round-to-minus-inf -
--round-to-nearest -
--round-to-plus-inf -
--round-to-zero -
--show-goto-functions -
--show-loops -
--show-properties -
--show-symbol-table -
--show-vcc -
--signed-overflow-check -
--slice-formula -
--smt2 -
--unsigned-char -
--unsigned-overflow-check -
--unwind -
--unwindset -
--yices -
--z3 -
-D -
-I