CBMC(1)

📦
version 6.8.0 · 5 versions
, in fedora 44, nixos 26.05

💖 CBMC(1) — User Commands 💖

okay bestie, welcome to cbmc, aka the Bounded Model Checker, living in section 1 of the manual (User Commands, if you were wondering) ✨ this is the girl who will literally tell you exactly how your assertion gets violated, or prove it can't be — within a given number of loop iterations. no cap. let's get into it 🫶

✨ NAME ✨

cbmc — Bounded Model Checker for C/C++ and Java programs 💅

🌈 SYNOPSIS 🌈

cbmc [--property property-id] file.c ...

cbmc [--show-properties] file.c ...

cbmc [--all-properties] file.c ...

cbmc [--no-standard-checks] file.c ...

cbmc [--no-standard-checks] [--pointer-check] file.c ...

cbmc [--no-bounds-check] file.c ...

goto-cc [-I include-path] [-c] file.c [-o outfile.o]

goto-instrument infile outfile

Only the most useful options are listed here; see below for the remainder. (yes she's holding out on you, there's SO much more, keep scrolling 📜)

🦋 DESCRIPTION 🦋

okay so here's the vibe: cbmc generates traces that demonstrate how an assertion can be violated, or proves that the assertion cannot be violated within a given number of loop iterations. like, she's not just gonna say "bad vibes detected" — she's gonna show you the receipts 🧾✨

CBMC can read C/C++ source-code directly, or a GOTO binary generated by goto-cc. Java programs? those come in as class or JAR files, slay 💅

Without any further options, cbmc checks all properties (automatically generated or user-specified) found in the program. If any of the properties can be violated, a counterexample is printed and the analysis is aborted 😭. The analysis can be restricted to a particular property with the --property option. The verification result for all properties can be obtained by means of the --all-properties option. obsessed.

goto-cc(1) reads source code, and generates a GOTO binary. Its command-line interface is designed to mimic that of gcc(1). Note in particular that goto-cc(1) distinguishes between compiling and linking phases, just as gcc does. cbmc expects a GOTO binary for which linking has been completed. (so like, finish the link, bestie, don't show up half-done 🙈)

goto-instrument(1) reads a GOTO binary, performs a given program transformation, and then writes the resulting program as GOTO binary on disc.

The usual flow is to:

  1. translate source into a GOTO binary using goto-cc,
  2. perform instrumentation with goto-instrument, and finally
  3. perform the analysis with cbmc.

it's giving ✨pipeline✨, it's giving main character energy 👑

💅 OPTIONS 💅

🌸 Standard Checks 🌸

From version 6.0 onwards, cbmc, goto-analyzer and some other tools apply some checks to the program by default (called the "standard checks"), with the aim to provide a better user experience for a non-expert user of the tool. These checks are:

  • --pointer-check — enable pointer checks
  • --bounds-check — enable array bounds checks
  • --undefined-shift-check — check shift greater than bit-width
  • --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
  • --pointer-primitive-check — checks that all pointers in pointer primitives are valid or null
  • --signed-overflow-check — enable signed arithmetic over- and underflow checks
  • --malloc-may-fail — allow malloc calls to return a null pointer
  • --malloc-fail-null — set malloc failure mode to return null
  • --unwinding-assertions — generate unwinding assertions (cannot be used with --cover)
⚠️ heads up: --unwinding-assertions cannot be used with --cover. they do NOT get along. it's a whole thing 💀

These checks can all be deactivated at once by using the --no-standard-checks flag like in the header example, or individually, by prepending a no- before the flag, like so:

  • --no-pointer-check — disable pointer checks
  • --no-bounds-check — disable array bounds checks
  • --no-undefined-shift-check — do not perform check for shift greater than bit-width
  • --no-div-by-zero-check — disable division by zero checks
  • --no-pointer-primitive-check — do not check that all pointers in pointer primitives are valid or null
  • --no-signed-overflow-check — disable signed arithmetic over- and underflow checks
  • --no-malloc-may-fail — do not allow malloc calls to fail by default
  • --no-unwinding-assertions — do not generate unwinding assertions

If an already set flag is re-set, like calling --pointer-check when default checks are already on, the flag is simply ignored. (she's unbothered, she's chill, she just moves on 🧚)

🎀 Analysis options: 🎀

  • --no-standard-checks — disable the standard (default) checks applied to a C/GOTO program (see above for more information)
  • --show-properties — show the properties, but don't run analysis
  • --symex-coverage-report f — generate a Cobertura XML coverage report in f
  • --property id — only check one specific property
  • --trace — give a counterexample trace for failed properties
  • --stop-on-fail — stop analysis once a failed property is detected (implies --trace)
  • --localize-faults — localize faults (experimental)

🍓 C/C++ frontend options: 🍓

  • --preprocess — stop after preprocessing
  • --test-preprocessor — stop after preprocessing, discard output
  • -I path — set include path (C/C++)
  • --include file — set include file (C/C++)
  • -D macro — define preprocessor macro (C/C++)
  • --c89, --c99, --c11, --c17, --c23 — set C language standard (default: c11)
  • --cpp98, --cpp03, --cpp11 — set C++ language standard (default: cpp98)
  • --unsigned-char — make "char" unsigned by default
  • --round-to-nearest, --round-to-even — rounding towards nearest even (default)
  • --round-to-plus-inf — rounding towards plus infinity
  • --round-to-minus-inf — rounding towards minus infinity
  • --round-to-zero — rounding towards zero
  • --no-library — disable built-in abstract C library
  • --max-nondet-tree-depth N — limit size of nondet (e.g. input) object tree; at level N pointers are set to null
  • --min-null-tree-depth N — minimum level at which a pointer can first be NULL in a recursively nondet initialized struct
  • --function name — set main function name

🌈 Platform options: 🌈

  • --arch arch — Set analysis architecture, which defaults to the host architecture. Use one of: alpha, arm, arm64, armel, armhf, hppa, i386, ia64, mips, mips64, mips64el, mipsel, mipsn32, mipsn32el, powerpc, ppc64, ppc64le, riscv64, s390, s390x, sh4, sparc, sparc64, v850, x32, x86_64, or none.
  • --os os — Set analysis operating system, which defaults to the host operating system. Use one of: freebsd, linux, macos, netbsd, openbsd, solaris, hurd, or windows.
  • --i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64 — Set analysis architecture and operating system.
  • --LP64, --ILP64, --LLP64, --ILP32, --LP32 — Set width of int, long and pointers, but don't override default architecture and operating system.
  • --16, --32, --64 — Equivalent to --LP32, --ILP32, --LP64 (on Windows: --LLP64).
  • --little-endian — allow little-endian word-byte conversions
  • --big-endian — allow big-endian word-byte conversions
  • --gcc — use GCC as preprocessor

🔥 Program representations: 🔥

  • --show-parse-tree — show parse tree
  • --show-symbol-table — show loaded symbol table
  • --show-goto-functions — show loaded goto program
  • --list-goto-functions — list loaded goto functions
  • --validate-goto-model — enable additional well-formedness checks on the goto program
  • --validate-ssa-equation — enable additional well-formedness checks on the SSA representation

🧚 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
  • --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)
  • --mm MM — memory consistency model for concurrent programs (default: sc)
  • --malloc-may-fail — allow malloc calls to return a null pointer
  • --malloc-fail-assert — set malloc failure mode to assert-then-assume
  • --malloc-fail-null — set malloc failure mode to return null
  • --string-abstraction — track C string lengths and zero-termination
  • --dfcc-debug-lib — enable debug assertions in the cprover contracts library
  • --dfcc-simple-invalid-pointer-model — use simplified invalid pointer model in the cprover contracts library (faster, unsound)
  • --reachability-slice — remove instructions that cannot appear on a trace from entry point to a property
  • --reachability-slice-fb — remove instructions that cannot appear on a trace from entry point through a property
  • --full-slice — run full slicer (experimental)
  • --drop-unused-functions — drop functions trivially unreachable from main function
💀 ngl, --dfcc-simple-invalid-pointer-model says the quiet part out loud: it's faster but also unsound. read the label, bestie.

👑 Semantic transformations: 👑

  • --nondet-static — add nondeterministic initialization of variables with static lifetime

⭐ BMC options: ⭐

  • --paths [strategy] — explore paths one at a time
  • --show-symex-strategies — list strategies for use with --paths
  • --show-goto-symex-steps — show which steps symex travels, includes diagnostic information
  • --show-points-to-sets — show points-to sets for pointer dereference. Requires --json-ui. ✨
  • --program-only — only show program expression. so minimal, so clean 💅
  • --show-byte-ops — show all byte extracts and updates. every lil byte gets its moment 🦋
  • --depth nr — limit search depth. nr is the depth cap, bestie.
  • --max-field-sensitivity-array-size M — maximum size M of arrays for which field sensitivity will be applied to array, the default is 64. iykyk
  • --no-array-field-sensitivity — deactivate field sensitivity for arrays, this is equivalent to setting the maximum field sensitivity size for arrays to 0. turn it off, turn it off 🫶
  • --show-loops — show the loops in the program. loop reveal, periodt 🔥
  • --unwind nr — unwind all loops at most nr times. give those loops a limit
  • --unwindset [T:]L:B,... — unwind loop L with a bound of B, optionally restricted to thread T, and overriding what may be set as default unwinding via --unwind (use --show-loops to get the loop IDs). very specific, very demure 💖
  • --incremental-loop L — check properties after each unwinding of loop L (use --show-loops to get the loop IDs). step by step, bestie ✨
  • --unwind-min nr — start incremental-loop after nr unwindings but before solving that iteration. If for example it is 1, then the loop will be unwound once, and immediately checked. Note: this means for min-unwind 1 or 0 all properties are checked. all the checks, no skips 😭
  • --unwind-max nr — stop incremental-loop after nr unwindings. okay that's enough 🛑
  • --ignore-properties-before-unwind-min — do not check properties before unwind-min when using incremental-loop. skip the pre-game 🙈
  • --show-vcc — show the verification conditions. the receipts, literally 🧾
  • --slice-formula — remove assignments unrelated to property. declutter that formula 🧹
  • --unwinding-assertions — generate unwinding assertions (which are enabled by default; overrides --no-unwinding-assertions when both of these are given); cannot be used with --cover. cannot be used with --cover so don't try it 💀
  • --partial-loops — permit paths that execute loops only partially (up to the given unwinding bound) and then continue beyond the loop even when the loop condition would still hold (such paths may be spurious, resulting in false alarms). warning: false alarms possible spooky 👻
  • --no-self-loops-to-assumptions — do not simplify while(1){} to assume(0). leave that loop alone 🫶
  • --symex-complexity-limit N — how complex (N) a path can become before symex abandons it. Currently uses guard size to calculate complexity. guard size is the vibe check ✨
  • --symex-complexity-failed-child-loops-limit N — how many child branches (N) in an iteration are allowed to fail due to complexity violations before the loop gets blacklisted. blacklisted, not me 💅
  • --graphml-witness filename — write the witness in GraphML format to filename. witness protection, but make it graph 🦋
  • --symex-cache-dereferences — enable caching of repeated dereferences. cache it, bestie 🎀

Backend options: 🛠️✨

  • --object-bits n — number of bits used for object addresses. n bits, no cap.
  • --sat-solver solver — use specified SAT solver. pick your fighter 💖
  • --external-sat-solver cmd — command to invoke SAT solver process. external, mysterious ✨
  • --no-sat-preprocessor — disable the SAT solver's simplifier. no simplifying today 🛑
  • --dimacs — generate CNF in DIMACS format. old school, iconic 📜
  • --beautify — beautify the counterexample (greedy heuristic). greedy but make it cute 💅
  • --smt1 — use default SMT1 solver (obsolete). obsolete, bestie 💀
  • --smt2 — use default SMT2 solver (Z3). Z3 is the moment 🔥
  • --bitwuzla — use Bitwuzla. say it with me: bit-wuz-la 🦋
  • --boolector — use Boolector. boo! 👻
  • --cprover-smt2 — use CPROVER SMT2 solver. CPROVER core ✨
  • --cvc3 — use CVC3. vintage 🎀
  • --cvc4 — use CVC4. a classic ⭐
  • --cvc5 — use CVC5. the new era 💖
  • --mathsat — use MathSAT. math but make it sat 🔥
  • --yices — use Yices. yices, yices, baby 💅
  • --z3 — use Z3. the people's solver 👑
  • --fpa — use theory of floating-point arithmetic. float like a butterfly 🦋
  • --external-smt2-solver cmd — Use cmd to invoke the SMT2 solver. Combine with one of the solver choices for solver-specific constraints. mix and match ✨
  • --refine — use refinement procedure (experimental). experimental handle with care 🫶
  • --refine-arrays — use refinement for arrays only. arrays only, periodt 💅
  • --refine-arithmetic — refinement of arithmetic expressions only. math only 🧮
  • --max-node-refinement — maximum refinement iterations for arithmetic expressions. cap it 🎀
  • --incremental-smt2-solver cmd — Use the incremental SMT backend where cmd is the command to invoke the SMT solver of choice. Example invocations:
--incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'
(use the CVC5 solver).

Note that:

  • The solver name must be in the "PATH" or be an executable with full path. full path or it's not invited
  • The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin. stdin only, bestie
  • The SMT solver should support the QF_AUFBV logic. QF_AUFBV or nothing 💖
  • --outfile filename — output formula to given file. save it 💾
  • --dump-smt-formula filename — output smt incremental formula to the given file. dump it, but fancy ✨
  • --write-solver-stats-to json-file — collect the solver query complexity. stats girlies rise 📊
  • --refine-strings — use string refinement (experimental). experimental strings attached 🎀
  • --string-printable — restrict to printable strings (experimental). experimental only printable, no weird vibes 🔥
  • --arrays-uf-never — never turn arrays into uninterpreted functions. never ever 🛑
  • --arrays-uf-always — always turn arrays into uninterpreted functions. always and forever 💅
  • --show-array-constraints — show array theory constraints added during post processing. Requires --json-ui. json-ui required, no cap ✨

User-interface options: 🎀✨

  • --xml-ui — use XML-formatted output. XML era 📜
  • --xml-interface — bi-directional XML interface. talk back in XML 🦋
  • --json-ui — use JSON-formatted output. JSON supremacy 👑
  • --json-interface — bi-directional JSON interface. JSON but make it chatty 💬
  • --trace-json-extended — add rawLhs property to trace. rawLhs, iconic 💅
  • --trace-show-function-calls — show function calls in plain trace. calls on display 📞
  • --trace-show-code — show original code in plain trace. the source, the drama 🎬
  • --trace-hex — represent plain trace values in hex. hex girl summer 🔥
  • --compact-trace — give a compact trace. compact, cute, contained 🎀
  • --stack-trace — give a stack trace only. just the stack, bestie 🥞
  • --flush — flush every line of output. flush it, don't hold back 🚽
  • --export-symex-ready-goto filename — export the symex ready version of the goto-model into the given filename. export the vibe ✨
  • --verbosity # — verbosity level. # is the level, no guessing 💖
  • --timestamp [monotonic|wall] — Print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601 wall clock timestamps. time is a construct, but microsecond-precision ⏰

ENVIRONMENT 🌍✨

All tools honor the TMPDIR environment variable when generating temporary files and directories. Furthermore note that the preprocessor used by cbmc will use environment variables to locate header files. env vars are the real main characters 💅

BUGS 🐛💖

If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues. report it, bestie, we don't suffer in silence 🫶

SEE ALSO 👀💅

goto-cc(1), goto-instrument(1) — the whole friend group ✨

2001-2016, Daniel Kroening, Edmund Clarke. respect the icons 👑

and that's the whole vibe, bestie. this page is from cbmc-5.59.0, dated June 2022. periodt. 💅✨

📦 where this page comes from