cprover
cbmc/module.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup module_cbmc CBMC tour
3 
4 \author Kareem Khazem
5 
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.
9 
10 
11 \dot
12 digraph G {
13 
14  rankdir="TB";
15  node [shape=box, fontcolor=blue];
16 
17  subgraph top {
18  rank=same;
19  1 -> 2 -> 3 -> 4;
20  }
21 
22  subgraph bottom {
23  rank=same;
24  5 -> 6 -> 7 -> 8 -> 9;
25  }
26 
27  /* shift bottom subgraph over */
28  9 -> 1 [color=white];
29 
30  4 -> 5;
31 
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"];
41 }
42 \enddot
43 
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
47 CBMC pipeline.