cbmc(1) on Linux
The text e60be3ce60cb, as Debian 13 (Trixie) shipped it. The page shows this text now.
Bounded Model Checker for C/C++ and Java programs
Flags it lists
-
--16 -
--32 -
--64 -
--ILP32 -
--ILP64 -
--LLP64 -
--LP32 -
--LP64 -
--arch -
--arrays-uf-always -
--arrays-uf-never -
--assert-to-assume -
--beautify -
--big-endian -
--bitwuzla -
--boolector -
--bounds-check -
--c11 -
--c17 -
--c23 -
--c89 -
--c99 -
--compact-trace -
--conversion-check -
--cover -
--cover-failed-assertions -
--cpp03 -
--cpp11 -
--cpp98 -
--cprover-smt2 -
--cvc3 -
--cvc4 -
--cvc5 -
--depth -
--dfcc-debug-lib -
--dfcc-simple-invalid-pointer-model -
--dimacs -
--div-by-zero-check -
--drop-unused-functions -
--dump-smt-formula -
--enum-range-check -
--error-label -
--export-symex-ready-goto -
--external-sat-solver -
--float-div-by-zero-check -
--float-overflow-check -
--flush -
--fpa -
--full-slice -
--function -
--gcc -
--graphml-witness -
--i386-linux -
--i386-macos -
--i386-win32 -
--ignore-properties-before-unwind-min -
--include -
--incremental-loop -
--incremental-smt2-solver -
--json-interface -
--json-ui -
--list-goto-functions -
--little-endian -
--localize-faults -
--malloc-fail-assert -
--malloc-fail-null -
--malloc-may-fail -
--mathsat -
--max-field-sensitivity-array-size -
--max-node-refinement -
--max-nondet-tree-depth -
--memory-cleanup-check -
--memory-leak-check -
--min-null-tree-depth -
--mm -
--nan-check -
--no-array-field-sensitivity -
--no-assertions -
--no-assumptions -
--no-bounds-check -
--no-built-in-assertions -
--no-div-by-zero-check -
--no-library -
--no-malloc-may-fail -
--no-pointer-check -
--no-pointer-primitive-check -
--no-sat-preprocessor -
--no-self-loops-to-assumptions -
--no-signed-overflow-check -
--no-standard-checks -
--no-undefined-shift-check -
--no-unwinding-assertions -
--nondet-static -
--object-bits -
--os -
--outfile -
--partial-loops -
--paths -
--pointer-check -
--pointer-overflow-check -
--pointer-primitive-check -
--ppc-macos -
--preprocess -
--program-only -
--property -
--reachability-slice -
--reachability-slice-fb -
--refine -
--refine-arithmetic -
--refine-arrays -
--refine-strings -
--retain-trivial-checks -
--round-to-even -
--round-to-minus-inf -
--round-to-nearest -
--round-to-plus-inf -
--round-to-zero -
--sat-solver -
--show-array-constraints -
--show-byte-ops -
--show-goto-functions -
--show-goto-symex-steps -
--show-loops -
--show-parse-tree -
--show-points-to-sets -
--show-properties -
--show-symbol-table -
--show-symex-strategies -
--show-test-suite -
--show-vcc -
--signed-overflow-check -
--slice-formula -
--smt1 -
--smt2 -
--stack-trace -
--stop-on-fail -
--string-abstraction -
--string-printable -
--symex-cache-dereferences -
--symex-complexity-failed-child-loops-limit -
--symex-complexity-limit -
--symex-coverage-report -
--test-preprocessor -
--timestamp -
--trace -
--trace-hex -
--trace-json-extended -
--trace-show-code -
--trace-show-function-calls -
--undefined-shift-check -
--unsigned-char -
--unsigned-overflow-check -
--unwind -
--unwind-max -
--unwind-min -
--unwinding-assertions -
--unwindset -
--validate-goto-model -
--validate-ssa-equation -
--verbosity -
--win32 -
--winx64 -
--write-solver-stats-to -
--xml-interface -
--xml-ui -
--yices -
--z3 -
-D -
-I