FreeBSD Manual Pages
CBMC(1) User Commands CBMC(1) 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. DESCRIPTION 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. CBMC can read C/C++ source-code directly, or a GOTO binary generated by goto-cc. Java programs are given as class or JAR files. Without any further options, cbmc checks all properties (automatically gen- erated 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. 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. goto-instrument(1) reads a GOTO binary, performs a given program transfor- mation, 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, then (2) perform instrumentation with goto-instrument, and finally (3) per- form the analysis with cbmc. 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) These checks can all be deactivated at once by using the --no-stan- dard-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. 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 ar- chitecture 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 as- sertion[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 de- fault 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 li- brary (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 Semantic transformations: --nondet-static add nondeterministic initialization of variables with static life- time 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 --show-byte-ops show all byte extracts and updates --depth nr limit search depth --max-field-sensitivity-array-size M maximum size M of arrays for which field sensitivity will be applied to array, the default is 64 --no-array-field-sensitivity deactivate field sensitivity for arrays, this is equivalent to set- ting the maximum field sensitivity size for arrays to 0 --show-loops show the loops in the program --unwind nr unwind all loops at most nr times --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) --incremental-loop L check properties after each unwinding of loop L (use --show-loops to get the loop IDs) --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. --unwind-max nr stop incremental-loop after nr unwindings --ignore-properties-before-unwind-min do not check properties before unwind-min when using incremen- tal-loop --show-vcc show the verification conditions --slice-formula remove assignments unrelated to property --unwinding-assertions generate unwinding assertions (which are enabled by default; over- rides --no-unwinding-assertions when both of these are given); can- not be used with --cover --partial-loops permit paths that execute loops only partially (up to the given un- winding bound) and then continue beyond the loop even when the loop condition would still hold (such paths may be spurious, resulting in false alarms) --no-self-loops-to-assumptions do not simplify while(1){} to assume(0) --symex-complexity-limit N how complex (N) a path can become before symex abandons it. Cur- rently uses guard size to calculate complexity. --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 --graphml-witness filename write the witness in GraphML format to filename --symex-cache-dereferences enable caching of repeated dereferences Backend options: --object-bits n number of bits used for object addresses --sat-solver solver use specified SAT solver --external-sat-solver cmd command to invoke SAT solver process --no-sat-preprocessor disable the SAT solver's simplifier --dimacs generate CNF in DIMACS format --beautify beautify the counterexample (greedy heuristic) --smt1 use default SMT1 solver (obsolete) --smt2 use default SMT2 solver (Z3) --bitwuzla use Bitwuzla --boolector use Boolector --cprover-smt2 use CPROVER SMT2 solver --cvc5 use CVC5 --mathsat use MathSAT --yices use Yices --z3 use Z3 --fpa use theory of floating-point arithmetic --external-smt2-solver cmd Use cmd to invoke the SMT2 solver. Combine with one of the solver choices for solver-specific constraints. --refine use refinement procedure (experimental) --refine-arrays use refinement for arrays only --refine-arithmetic refinement of arithmetic expressions only --max-node-refinement maximum refinement iterations for arithmetic expressions --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. The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin. The SMT solver should support the QF_AUFBV logic. --outfile filename output formula to given file --dump-smt-formula filename output smt incremental formula to the given file --write-solver-stats-to json-file collect the solver query complexity --refine-strings use string refinement (experimental) --string-printable restrict to printable strings (experimental) --arrays-uf-never never turn arrays into uninterpreted functions --arrays-uf-always always turn arrays into uninterpreted functions --show-array-constraints show array theory constraints added during post processing. Re- quires --json-ui. User-interface options: --xml-ui use XML-formatted output --xml-interface bi-directional XML interface --json-ui use JSON-formatted output --json-interface bi-directional JSON interface --trace-json-extended add rawLhs property to trace --trace-show-function-calls show function calls in plain trace --trace-show-code show original code in plain trace --trace-hex represent plain trace values in hex --compact-trace give a compact trace --stack-trace give a stack trace only --flush flush every line of output --export-symex-ready-goto filename export the symex ready version of the goto-model into the given filename --verbosity # verbosity level --timestamp [monotonic|wall] Print microsecond-precision timestamps. monotonic: stamps increase monotonically. wall: ISO-8601 wall clock timestamps. 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. BUGS If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues SEE ALSO goto-cc(1), goto-instrument(1) COPYRIGHT 2001-2016, Daniel Kroening, Edmund Clarke cbmc-5.59.0 June 2022 CBMC(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | ENVIRONMENT | BUGS | SEE ALSO | COPYRIGHT
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=cbmc&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>