CBMC and JBMC Documentation

The src/ directory is organized into functional modules. Understanding this structure helps in locating specific components of the toolchain:

• GOTO-Programs: Core intermediate representation and linking logic.
• Symbolic Execution: Components like goto-checker and goto-symex.
• Static Analyses: Includes pointer analysis and other analysis engines.
• Solvers: Interface and logic for interacting with solvers.
• Language Front Ends: Support for C, C++, and Java bytecode.
• Tools: The primary executables such as cbmc, goto-cc, goto-analyzer, goto-instrument, goto-diff, goto-harness, and jbmc.
• Utilities: Low-level libraries for JSON, XML, big integers, and more.

JBMC is a bounded model checking tool for the Java language. It performs static analysis and symbolic execution on Java Bytecode (provided as .class files or .jar files) to prove or refute properties.

Properties are handled in two ways:

1. Automatic assertions: JBMC automatically checks for runtime errors (e.g., null pointer exceptions, array index out of bounds).
2. User assertions: Users can provide explicit assert statements in their code for JBMC to verify.

JBMC follows the same principles as CBMC.

The C++ front-end is designed to support the subset of C++ typically used in embedded and system applications. It functions by parsing C++ code and converting it into goto-programs, utilizing code from langapi and ansi-c.

Limitations: Because it targets a specific subset of the language, it does not provide full support for templates or many advanced/obscure C++ features. The supported language subset is continuously being extended.

CBMC supports formal code contracts to specify the behavior of functions and loops. Contracts allow you to define preconditions, postconditions, and other properties that the verifier uses to prove the correctness of your code.

Key areas of contract specification include:

• Function Contracts: Defining requirements and guarantees for function execution (e.g., requires, ensures, assigns).
• Loop Contracts: Defining properties that hold true during loop execution (e.g., loop-invariants, decreases).
• Advanced Predicates: Using memory predicates, function pointer predicates, and quantifiers for complex specifications.

goto-cc is a compiler replacement tool that performs the initial step of converting C or C++ programs into goto-binaries.

It is designed to be integrated into existing build procedures by replacing the standard compiler. To ensure the resulting binary emulates the semantics of specific compilers, you must name the goto-cc binary according to the compiler you wish to emulate. The output binaries produced by goto-cc are compatible with cbmc and goto-instrument.

The CPROVER subversion archive includes several specialized programs for model checking, instrumentation, and test generation. While many interfaces are stabilizing, users should be aware that older code may require adjustments to compile or function correctly.

Core Archive Tools

• CBMC: A bounded model checking tool for C and C++.
• goto-cc: A drop-in, flag-compatible replacement for GCC and other compilers. Instead of producing executable binaries, it produces goto-programs.
• goto-instrument: A collection of functions used for instrumenting and modifying goto-programs.

The ANSI C module provides a front-end for parsing ANSI C code and its common extensions. It uses a traditional Flex/Bison parser to transform C source files into a 'goto-program'.

Key features include:

• Magic Functions: Implementation in internal_addition.c allows controlling analysis directly from source code via assertions, assumptions, atomic blocks, memory fences, and rounding modes.
• CPROVER-aware Libraries: The library/ directory contains C standard header files (e.g., stdio.c, string.c, setjmp.c, and threading interfaces) that use CPROVER built-in functions to model standard functionality correctly for analysis.

CBMC is a Bounded Model Checker for C and C++ programs. It verifies properties such as array bounds (buffer overflows), pointer safety, exceptions, and user-specified assertions.

Key capabilities:

• Supports C89, C99, most of C11, C17, C23, and common compiler extensions from gcc and Visual Studio.
• Supports SystemC via Scoot.
• Can check C and C++ for consistency with other languages like Verilog.
• Verification works by unwinding program loops and passing the resulting equations to a decision procedure.