Author: Martin Brain, Peter Schrammel

This section provides a graphical overview of how CBMC fits together. CBMC takes C code or a goto-binary as input and tries to emit traces of executions that lead to crashes or undefined behaviour. The diagram below shows the intermediate steps in this process.

The CPROVER User Manual describes CBMC from a user perspective. Each node in the diagram above links to the appropriate class or module documentation, describing that particular stage in the CBMC pipeline. CPROVER is structured in a similar fashion to a compiler. It has language specific front-ends which perform limited syntactic analysis and then convert to an intermediate format. The intermediate format can be output to files (this is what goto-cc does) and are (informally) referred to as “goto binaries” or “goto programs”. The back-end are tools process this format, either directly from the front-end or from it’s saved output. These include a wide range of analysis and transformation tools (see Other Tools).

Concepts

Central data structures

For an explanation of the data structures involved in the modeling of a GOTO program (the GOTO Intermediate Representation used by CBMC and assorted tools) please see Central Data Structures .

{C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing

To be documented.

Instrumentation: goto functions → goto functions

For an overview of the transformations applied to goto programs after the generation of the initial goto program and before BMC, see Goto Program Transformations .

To be documented.

Goto functions → BMC → Counterexample (trace)

For an explanation of part of how the BMC (Symex) process works, please refer to Symex and GOTO program instructions

Trace → interpreter → memory map

To be documented.

Goto functions → abstract interpretation

To be documented.

Executables (flow of transformations):

goto-cc

To be documented.

goto-instrument

To be documented.

cbmc

To be documented.

goto-analyzer

To be documented.

Last modified: 2024-04-26 11:55:11 +0200