Skip to content

Commit d9e690b

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 2939db4 commit d9e690b

File tree

2 files changed

+89
-83
lines changed

2 files changed

+89
-83
lines changed

doc/architectural/CBMC-developer-guide.md

Lines changed: 1 addition & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -185,89 +185,7 @@ To be documented.
185185

186186
\section section-folder-walkthrough Folder walkthrough
187187

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

272190

273191

Lines changed: 88 additions & 0 deletions
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)