cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/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 clobber
39  * \ref goto-analyzer
40  * \ref goto-instrument
41  * \ref goto-diff
42  * \ref memory-models
43  * \ref goto-cc
44  * \ref jbmc
45 
46 - Utilities
47 
48  * \ref big-int
49  * \ref json
50  * \ref xmllang
51  * \ref util
52  * \ref miniz
53  * \ref nonstd
54 
55 In the top level of `src` there are only a few files:
56 
57 * `config.inc`: The user-editable configuration parameters for the
58  build process. The main use of this file is setting the paths for the
59  various external SAT solvers that are used. As such, anyone building
60  from source will likely need to edit this.
61 
62 * `Makefile`: The main systems Make file. Parallel builds are
63  supported and encouraged; please don’t break them!
64 
65 * `common`: System specific magic required to get the system to build.
66  This should only need to be edited if porting CBMC to a new platform /
67  build environment.
68 
69 * `doxygen.cfg`: The config file for doxygen.cfg
70 
71 ## `doc/` ##
72 
73 Contains the CBMC man page. Doxygen HTML pages are generated
74 into the `doc/html` directory when running `doxygen` from `src`.
75 
76 ## `regression/` ##
77 
78 The `regression/` directory contains the regression test suites. See
79 \ref compilation-and-development for information on how to run and
80 develop regression tests.
81 
82 ## `unit/` ##
83 
84 The `unit/` directory contains the unit test suites. See
85 \ref compilation-and-development for information on how to run and
86 develop unit tests.