2 \page folder-walkthrough Folder Walkthrough
4 \author Martin Brain, Peter Schrammel
8 The source code is divided into a number of sub-directories, each
9 containing the code for a different part of the system.
22 * \ref pointer-analysis
29 * Language API: \ref langapi
32 * Java: \ref java_bytecode
33 * JavaScript: \ref jsil
39 * \ref goto-instrument
53 In the top level of `src` there are only a few files:
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.
60 * `Makefile`: The main systems Make file. Parallel builds are
61 supported and encouraged; please don’t break them!
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 /
67 * `doxygen.cfg`: The config file for doxygen.cfg
71 Contains the CBMC man page. Doxygen HTML pages are generated
72 into the `doc/html` directory when running `doxygen` from `src`.
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.
82 The `unit/` directory contains the unit test suites. See
83 \ref compilation-and-development for information on how to run and
86 ## Directory dependencies ##
88 This diagram shows *intended* directory dependencies. Arrows should
89 be read transitively - dependencies of dependencies are often used
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.
98 digraph directory_dependencies {
99 node [style = filled, color = white];
101 subgraph cluster_executables {
102 label = "Executables";
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"];
117 subgraph cluster_symbolic_execution {
118 label = "Symbolic Execution";
121 node [style = filled, color = white];
122 goto_symex [label = "goto-symex", URL = "\ref goto-symex"];
125 subgraph cluster_abstract_interpretation {
126 label = "Abstract Interpretation";
129 node [style = filled, color = white];
130 pointer_analysis [label = "pointer-analysis", URL = "\ref pointer-analysis"];
131 analyses [URL = "\ref analyses"];
134 subgraph cluster_goto_programs {
135 label = "Goto Programs";
138 goto_programs [label = "goto-programs", URL = "\ref goto-programs"];
139 linking [URL = "\ref linking"];
142 subgraph cluster_solvers {
146 solvers [URL = "\ref solvers"];
149 subgraph cluster_languages {
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"];
160 subgraph cluster_utilities {
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"];
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;
183 java_bytecode -> { analyses, miniz };
187 langapi -> goto_programs;
189 goto_symex -> { solvers, pointer_analysis };
191 pointer_analysis -> { analyses, goto_programs };
192 analyses -> pointer_analysis;
196 linking -> goto_programs;
197 goto_programs -> { linking, xmllang, json, assembler };