2 \page cbmc-architecture CBMC Architecture
4 \author Martin Brain, Peter Schrammel
6 This section provides a graphical overview of how CBMC fits together.
7 CBMC takes C code or a goto-binary as input and tries to emit traces
8 of executions that lead to crashes or undefined behaviour. The diagram
9 below shows the intermediate steps in this process.
15 node [shape=box, fontcolor=blue];
24 5 -> 6 -> 7 -> 8 -> 9;
27 /* shift bottom subgraph over */
32 1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
33 2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
34 3 [label="language\ntype-checking" URL="\ref type-checking"];
35 4 [label="goto\nconversion" URL="\ref goto-conversion"];
36 5 [label="instrumentation" URL="\ref instrumentation"];
37 6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
38 7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
39 8 [label="decision\nprocedure" URL="\ref decision-procedure"];
40 9 [label="counter example\nproduction" URL="\ref counter-example-production"];
44 The \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
45 perspective. Each node in the diagram above links to the appropriate
46 class or module documentation, describing that particular stage in the
48 CPROVER is structured in a similar fashion to a compiler. It has
49 language specific front-ends which perform limited syntactic analysis
50 and then convert to an intermediate format. The intermediate format can
51 be output to files (this is what `goto-cc` does) and are (informally)
52 referred to as “goto binaries” or “goto programs”. The back-end are
53 tools process this format, either directly from the front-end or from
54 it’s saved output. These include a wide range of analysis and
55 transformation tools (see \ref section-other-tools).
58 ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
62 ## Instrumentation: goto functions → goto functions ##
66 ## Goto functions → BMC → Counterexample (trace) ##
70 ## Trace → interpreter → memory map ##
74 ## Goto functions → abstract interpretation ##
78 ## Executables (flow of transformations): ##
84 ### goto-instrument ###