cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/code-walkthrough.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page code-walkthrough Code Walkthrough
3 
4 \author Cesar Rodriguez, Owen Jones
5 
6 \section data-structures-core-structures-and-ast-section Data structures: core structures and AST
7 
8 The core structures used for representing abstract syntax trees are all
9 documented in \ref util.
10 
11 \section data-structures-from-ast-to-goto-program-section Data structures: from AST to GOTO program
12 
13 See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt::instructiont).
14 
15 \section front-end-languages-generating-codet-from-multiple-languages-section Front-end languages: generating codet from multiple languages
16 
17 \subsection language-uit-section language_uit, language_filest, languaget classes:
18 
19 See \ref langapi.
20 
21 \subsection languages-c-section C
22 
23 See \ref ansi-c.
24 
25 \subsection languages-cpp-section C++
26 
27 See \ref cpp.
28 
29 \subsection languages-java-section Java bytecode
30 
31 See \ref java_bytecode.
32 
33 \section bmct-class-section Bmct class
34 
35 \subsection equation-section equation
36 
37 See \ref symex-overview.
38 
39 
40 \section symbolic-executors-section Symbolic executors
41 
42 \subsection symbolic-execution-section Symbolic execution
43 
44 See \ref symex-overview.
45 
46 
47 \section solvers-infrastructure-section Solvers infrastructure
48 
49 See \ref solvers-overview.
50 
51 \section static-analysis-apis-section Static analysis APIs
52 
53 See \ref analyses and \ref pointer-analysis.