* * CBMC 6.11.0 (cbmc-6.11.0-dirty) 64-bit * * * * Copyright (C) 2001-2018 * * * * Daniel Kroening, Edmund Clarke * * * * Carnegie Mellon University, Computer Science Department * * * * kroening@kroening.com * * * * Protected in part by U.S. patent 7,225,417 * * Usage: Purpose: cbmc [-?] [-h] [--help] show this help cbmc --version show version and exit cbmc [options] file.c ... perform bounded model checking Analysis options: --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_name set architecture (default: x86_64) to 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_name set operating system (default: linux) to one of: freebsd, linux, macos, netbsd, openbsd, solaris, hurd, or windows --i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64 set 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 --export-symex-ready-goto f serialise goto-program in symex-ready-goto form in f Program instrumentation options: --no-standard-checks disable default checks (more information in manpage) --bounds-check enable array bounds checks (default on) --no-bounds-check disable array bounds checks --pointer-check enable pointer checks (default on) --no-pointer-check disable pointer checks --memory-leak-check enable memory leak checks --memory-cleanup-check enable memory cleanup checks --div-by-zero-check enable division by zero checks on integers (default on) --float-div-by-zero-check enable division by zero checks on floating-point numbers (default off) --no-div-by-zero-check disable division by zero checks --signed-overflow-check enable signed arithmetic over- and underflow checks (default on) --no-signed-overflow-check disable 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 (default on) --no-undefined-shift-check disable check for 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 (default on) --no-pointer-primitive-check disable 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 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 --no-malloc-may-fail disable potential malloc failure --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-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 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 --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 setting the maximum field sensitivity size for arrays to 0 --show-loops show the loops in the program --unwind nr unwind loops nr times --unwindset [T:]L:B,... unwind loop L with a bound of B (optionally restricted to thread T) (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 --unwind-min 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 --incremental-loop --show-vcc show the verification conditions --slice-formula remove assignments unrelated to property --unwinding-assertions generate unwinding assertions (cannot be used with --cover) --partial-loops permit paths with partial loops --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. Currently 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 command to invoke 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 command to invoke external SMT solver for incremental solving (experimental) --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. Requires --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 --verbosity # verbosity level (default 6) --timestamp [monotonic|wall] print microsecond-precision timestamps. monotonic : stamps increase monotonically. wall: ISO-8601 wall clock timestamps.