2 \defgroup module_cbmc CBMC tour
6 CBMC takes C code or a goto-binary as input and tries to emit traces of
7 executions that lead to crashes or undefined behaviour. The diagram
8 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 cprover-manual "CProver 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