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

{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

To be documented.

Goto functions → BMC → Counterexample (trace)

To be documented.

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: 2022-09-29 15:10:20 -0400