cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/folder-walkthrough.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page folder-walkthrough Folder Walkthrough
3 
4 \author Martin Brain, Peter Schrammel
5 
6 ## `src/` ##
7 
8 The source code is divided into a number of sub-directories, each
9 containing the code for a different part of the system.
10 
11 - GOTO-Programs
12 
13  * \ref goto-programs
14  * \ref linking
15 
16 - Symbolic Execution
17  * \ref goto-symex
18 
19 - Static Analyses
20 
21  * \ref analyses
22  * \ref pointer-analysis
23 
24 - Solvers
25  * \ref solvers
26 
27 - Language Front Ends
28 
29  * Language API: \ref langapi
30  * C: \ref ansi-c
31  * C++: \ref cpp
32  * Java: \ref java_bytecode
33  * JavaScript: \ref jsil
34 
35 - Tools
36 
37  * \ref cbmc
38  * \ref goto-analyzer
39  * \ref goto-instrument
40  * \ref goto-diff
41  * \ref goto-cc
42  * \ref jbmc
43 
44 - Utilities
45 
46  * \ref big-int
47  * \ref json
48  * \ref xmllang
49  * \ref util
50  * \ref miniz
51  * \ref nonstd
52 
53 In the top level of `src` there are only a few files:
54 
55 * `config.inc`: The user-editable configuration parameters for the
56  build process. The main use of this file is setting the paths for the
57  various external SAT solvers that are used. As such, anyone building
58  from source will likely need to edit this.
59 
60 * `Makefile`: The main systems Make file. Parallel builds are
61  supported and encouraged; please don’t break them!
62 
63 * `common`: System specific magic required to get the system to build.
64  This should only need to be edited if porting CBMC to a new platform /
65  build environment.
66 
67 * `doxygen.cfg`: The config file for doxygen.cfg
68 
69 ## `doc/` ##
70 
71 Contains the CBMC man page. Doxygen HTML pages are generated
72 into the `doc/html` directory when running `doxygen` from `src`.
73 
74 ## `regression/` ##
75 
76 The `regression/` directory contains the regression test suites. See
77 \ref compilation-and-development for information on how to run and
78 develop regression tests.
79 
80 ## `unit/` ##
81 
82 The `unit/` directory contains the unit test suites. See
83 \ref compilation-and-development for information on how to run and
84 develop unit tests.
85 
86 ## Directory dependencies ##
87 
88 This diagram shows *intended* directory dependencies. Arrows should
89 be read transitively - dependencies of dependencies are often used
90 directly.
91 
92 There are `module_dependencies.txt` files in each directory,
93 which are checked by the linter. Where directories in `module_dependencies.txt`
94 are marked with comments such as 'dubious' or 'should go away', these
95 dependencies have generally not been included in the diagram.
96 
97 \dot
98 digraph directory_dependencies {
99  node [style = filled, color = white];
100 
101  subgraph cluster_executables {
102  label = "Executables";
103  style = filled;
104  color = lightgrey;
105  node [style = filled, color = white];
106  CBMC [URL = "\ref cbmc"];
107  goto_cc [label = "goto-cc", URL = "\ref goto-cc"];
108  goto_analyzer [label = "goto-analyzer", URL = "\ref goto-analyzer"];
109  goto_instrument [label = "goto-instrument", URL = "\ref goto-instrument"];
110  goto_diff [label = "goto-diff", URL = "\ref goto-diff"];
111  janalyzer [URL = "\ref janalyzer"];
112  jdiff [URL = "\ref jdiff"];
113  JBMC [URL = "\ref jbmc"];
114  smt2_solver;
115  }
116 
117  subgraph cluster_symbolic_execution {
118  label = "Symbolic Execution";
119  style = filled;
120  color = lightgrey;
121  node [style = filled, color = white];
122  goto_symex [label = "goto-symex", URL = "\ref goto-symex"];
123  }
124 
125  subgraph cluster_abstract_interpretation {
126  label = "Abstract Interpretation";
127  style = filled;
128  color = lightgrey;
129  node [style = filled, color = white];
130  pointer_analysis [label = "pointer-analysis", URL = "\ref pointer-analysis"];
131  analyses [URL = "\ref analyses"];
132  }
133 
134  subgraph cluster_goto_programs {
135  label = "Goto Programs";
136  style = filled;
137  color = lightgrey;
138  goto_programs [label = "goto-programs", URL = "\ref goto-programs"];
139  linking [URL = "\ref linking"];
140  }
141 
142  subgraph cluster_solvers {
143  label = "Solvers"
144  style = filled;
145  color = lightgrey;
146  solvers [URL = "\ref solvers"];
147  }
148 
149  subgraph cluster_languages {
150  label = "Languages";
151  style = filled;
152  color = lightgrey;
153  ansi_c [label = "ansi-c", URL = "\ref ansi-c"];
154  langapi [URL = "\ref langapi"];
155  cpp [URL = "\ref cpp"];
156  jsil [URL = "\ref jsil"];
157  java_bytecode [URL = "\ref java_bytecode"];
158  }
159 
160  subgraph cluster_utilities {
161  label = "Utilities";
162  style = filled;
163  color = lightgrey;
164  big_int [label = "big-int", URL = "\ref big-int"];
165  miniz [URL = "\ref miniz"];
166  util [URL = "\ref util"];
167  nonstd [URL = "\ref nonstd"];
168  json [URL = "\ref json"];
169  xmllang [URL = "\ref xmllang"];
170  assembler [URL = "\ref assembler"];
171  }
172 
173  JBMC -> { CBMC, java_bytecode };
174  jdiff -> { goto_diff, java_bytecode };
175  janalyzer -> { goto_analyzer, java_bytecode };
176  CBMC -> { goto_instrument, jsil };
177  goto_diff -> { goto_instrument };
178  goto_analyzer -> { analyses, jsil, cpp };
179  goto_instrument -> { goto_symex, cpp };
180  goto_cc -> { cpp, jsil };
181  smt2_solver -> solvers;
182 
183  java_bytecode -> { analyses, miniz };
184  jsil -> linking;
185  cpp -> ansi_c;
186  ansi_c -> langapi;
187  langapi -> goto_programs;
188 
189  goto_symex -> { solvers, pointer_analysis };
190 
191  pointer_analysis -> { analyses, goto_programs };
192  analyses -> pointer_analysis;
193 
194  solvers -> util;
195 
196  linking -> goto_programs;
197  goto_programs -> { linking, xmllang, json, assembler };
198 
199  json -> util;
200  xmllang -> util;
201  assembler -> util;
202  util -> big_int;
203  util -> nonstd;
204 }
205 \enddot