Skip to content

Commit a88f851

Browse files
author
Owen Jones
committed
Move folder walkthrough to a separate file
The CBMC Developer Guide now contains a link to that file.
1 parent be3d22f commit a88f851

File tree

2 files changed

+89
-83
lines changed

2 files changed

+89
-83
lines changed

doc/architectural/CBMC-developer-guide.md

+1-83
Original file line numberDiff line numberDiff line change
@@ -187,89 +187,7 @@ To be documented. (Martin?)
187187

188188
\section section-folder-walkthrough Folder walkthrough
189189

190-
## `src/` ##
191-
192-
The source code is divided into a number of sub-directories, each
193-
containing the code for a different part of the system.
194-
195-
- GOTO-Programs
196-
197-
* \ref goto-programs
198-
* \ref linking
199-
200-
- Symbolic Execution
201-
* \ref goto-symex
202-
203-
- Static Analyses
204-
205-
* \ref analyses
206-
* \ref pointer-analysis
207-
208-
- Solvers
209-
* \ref solvers
210-
211-
- Language Front Ends
212-
213-
* Language API: \ref langapi
214-
* C: \ref ansi-c
215-
* C++: \ref cpp
216-
* Java: \ref java_bytecode
217-
* JavaScript: \ref jsil
218-
219-
- Tools
220-
221-
* \ref cbmc
222-
* \ref clobber
223-
* \ref goto-analyzer
224-
* \ref goto-instrument
225-
* \ref goto-diff
226-
* \ref memory-models
227-
* \ref goto-cc
228-
* \ref jbmc
229-
230-
- Utilities
231-
232-
* \ref big-int
233-
* \ref json
234-
* \ref xmllang
235-
* \ref util
236-
* \ref miniz
237-
* \ref nonstd
238-
239-
In the top level of `src` there are only a few files:
240-
241-
* `config.inc`: The user-editable configuration parameters for the
242-
build process. The main use of this file is setting the paths for the
243-
various external SAT solvers that are used. As such, anyone building
244-
from source will likely need to edit this.
245-
246-
* `Makefile`: The main systems Make file. Parallel builds are
247-
supported and encouraged; please don’t break them!
248-
249-
* `common`: System specific magic required to get the system to build.
250-
This should only need to be edited if porting CBMC to a new platform /
251-
build environment.
252-
253-
* `doxygen.cfg`: The config file for doxygen.cfg
254-
255-
## `doc/` ##
256-
257-
Contains the CBMC man page. Doxygen HTML pages are generated
258-
into the `doc/html` directory when running `doxygen` from `src`.
259-
260-
## `regression/` ##
261-
262-
The `regression/` directory contains the test suites.
263-
They are grouped into directories for each of the tools/modules.
264-
Each of these contains a directory per test case, containing a C or C++
265-
file that triggers the bug and a `.desc` file that describes
266-
the tests, expected output and so on. There is a Perl script,
267-
`test.pl` that is used to invoke the tests as:
268-
269-
../test.pl -c PATH_TO_CBMC
270-
271-
The `–help` option gives instructions for use and the
272-
format of the description files.
190+
See [the folder walkthrough](folder-walkthrough.md).
273191

274192

275193

+88
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
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 test suites.
79+
They are grouped into directories for each of the tools/modules.
80+
Each of these contains a directory per test case, containing a C or C++
81+
file that triggers the bug and a `.desc` file that describes
82+
the tests, expected output and so on. There is a Perl script,
83+
`test.pl` that is used to invoke the tests as:
84+
85+
../test.pl -c PATH_TO_CBMC
86+
87+
The `–help` option gives instructions for use and the
88+
format of the description files.

0 commit comments

Comments
 (0)