Skip to content

Commit b368ca4

Browse files
author
Mark R. Tuttle
committed
Add top-level documtation pages
Add top-level user guide, reference guide, developer guide pages for the new published documentation. The top-level doxyfile is the original src/doxyfile with minor modification (eg, project title is now "CBMC").
1 parent 8cae33b commit b368ca4

11 files changed

+2827
-0
lines changed

‎doc/doxygen-root/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
html/

‎doc/doxygen-root/DoxygenLayout.xml

Lines changed: 194 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,194 @@
1+
<doxygenlayout version="1.0">
2+
<!-- Generated by doxygen 1.8.15 -->
3+
<!-- Navigation index tabs for HTML output -->
4+
<navindex>
5+
<tab type="mainpage" visible="yes" title=""/>
6+
<tab type="pages" visible="yes" title="" intro=""/>
7+
<tab type="modules" visible="yes" title="Directories" intro=""/>
8+
<tab type="namespaces" visible="yes" title="">
9+
<tab type="namespacelist" visible="yes" title="" intro=""/>
10+
<tab type="namespacemembers" visible="yes" title="" intro=""/>
11+
</tab>
12+
<tab type="classes" visible="yes" title="">
13+
<tab type="classlist" visible="yes" title="" intro=""/>
14+
<tab type="classindex" visible="$ALPHABETICAL_INDEX" title=""/>
15+
<tab type="hierarchy" visible="yes" title="" intro=""/>
16+
<tab type="classmembers" visible="yes" title="" intro=""/>
17+
</tab>
18+
<tab type="files" visible="yes" title="">
19+
<tab type="filelist" visible="yes" title="" intro=""/>
20+
<tab type="globals" visible="yes" title="" intro=""/>
21+
</tab>
22+
<tab type="examples" visible="yes" title="" intro=""/>
23+
</navindex>
24+
25+
<!-- Layout definition for a class page -->
26+
<class>
27+
<briefdescription visible="yes"/>
28+
<includes visible="$SHOW_INCLUDE_FILES"/>
29+
<inheritancegraph visible="$CLASS_GRAPH"/>
30+
<collaborationgraph visible="$COLLABORATION_GRAPH"/>
31+
<memberdecl>
32+
<nestedclasses visible="yes" title=""/>
33+
<publictypes title=""/>
34+
<services title=""/>
35+
<interfaces title=""/>
36+
<publicslots title=""/>
37+
<signals title=""/>
38+
<publicmethods title=""/>
39+
<publicstaticmethods title=""/>
40+
<publicattributes title=""/>
41+
<publicstaticattributes title=""/>
42+
<protectedtypes title=""/>
43+
<protectedslots title=""/>
44+
<protectedmethods title=""/>
45+
<protectedstaticmethods title=""/>
46+
<protectedattributes title=""/>
47+
<protectedstaticattributes title=""/>
48+
<packagetypes title=""/>
49+
<packagemethods title=""/>
50+
<packagestaticmethods title=""/>
51+
<packageattributes title=""/>
52+
<packagestaticattributes title=""/>
53+
<properties title=""/>
54+
<events title=""/>
55+
<privatetypes title=""/>
56+
<privateslots title=""/>
57+
<privatemethods title=""/>
58+
<privatestaticmethods title=""/>
59+
<privateattributes title=""/>
60+
<privatestaticattributes title=""/>
61+
<friends title=""/>
62+
<related title="" subtitle=""/>
63+
<membergroups visible="yes"/>
64+
</memberdecl>
65+
<detaileddescription title=""/>
66+
<memberdef>
67+
<inlineclasses title=""/>
68+
<typedefs title=""/>
69+
<enums title=""/>
70+
<services title=""/>
71+
<interfaces title=""/>
72+
<constructors title=""/>
73+
<functions title=""/>
74+
<related title=""/>
75+
<variables title=""/>
76+
<properties title=""/>
77+
<events title=""/>
78+
</memberdef>
79+
<allmemberslink visible="yes"/>
80+
<usedfiles visible="$SHOW_USED_FILES"/>
81+
<authorsection visible="yes"/>
82+
</class>
83+
84+
<!-- Layout definition for a namespace page -->
85+
<namespace>
86+
<briefdescription visible="yes"/>
87+
<memberdecl>
88+
<nestednamespaces visible="yes" title=""/>
89+
<constantgroups visible="yes" title=""/>
90+
<classes visible="yes" title=""/>
91+
<typedefs title=""/>
92+
<enums title=""/>
93+
<functions title=""/>
94+
<variables title=""/>
95+
<membergroups visible="yes"/>
96+
</memberdecl>
97+
<detaileddescription title=""/>
98+
<memberdef>
99+
<inlineclasses title=""/>
100+
<typedefs title=""/>
101+
<enums title=""/>
102+
<functions title=""/>
103+
<variables title=""/>
104+
</memberdef>
105+
<authorsection visible="yes"/>
106+
</namespace>
107+
108+
<!-- Layout definition for a file page -->
109+
<file>
110+
<briefdescription visible="yes"/>
111+
<includes visible="$SHOW_INCLUDE_FILES"/>
112+
<includegraph visible="$INCLUDE_GRAPH"/>
113+
<includedbygraph visible="$INCLUDED_BY_GRAPH"/>
114+
<sourcelink visible="yes"/>
115+
<memberdecl>
116+
<classes visible="yes" title=""/>
117+
<namespaces visible="yes" title=""/>
118+
<constantgroups visible="yes" title=""/>
119+
<defines title=""/>
120+
<typedefs title=""/>
121+
<enums title=""/>
122+
<functions title=""/>
123+
<variables title=""/>
124+
<membergroups visible="yes"/>
125+
</memberdecl>
126+
<detaileddescription title=""/>
127+
<memberdef>
128+
<inlineclasses title=""/>
129+
<defines title=""/>
130+
<typedefs title=""/>
131+
<enums title=""/>
132+
<functions title=""/>
133+
<variables title=""/>
134+
</memberdef>
135+
<authorsection/>
136+
</file>
137+
138+
<!-- Layout definition for a group page -->
139+
<group>
140+
<briefdescription visible="yes"/>
141+
<groupgraph visible="$GROUP_GRAPHS"/>
142+
<memberdecl>
143+
<nestedgroups visible="yes" title=""/>
144+
<dirs visible="yes" title=""/>
145+
<files visible="yes" title=""/>
146+
<namespaces visible="yes" title=""/>
147+
<classes visible="yes" title=""/>
148+
<defines title=""/>
149+
<typedefs title=""/>
150+
<enums title=""/>
151+
<enumvalues title=""/>
152+
<functions title=""/>
153+
<variables title=""/>
154+
<signals title=""/>
155+
<publicslots title=""/>
156+
<protectedslots title=""/>
157+
<privateslots title=""/>
158+
<events title=""/>
159+
<properties title=""/>
160+
<friends title=""/>
161+
<membergroups visible="yes"/>
162+
</memberdecl>
163+
<detaileddescription title=""/>
164+
<memberdef>
165+
<pagedocs/>
166+
<inlineclasses title=""/>
167+
<defines title=""/>
168+
<typedefs title=""/>
169+
<enums title=""/>
170+
<enumvalues title=""/>
171+
<functions title=""/>
172+
<variables title=""/>
173+
<signals title=""/>
174+
<publicslots title=""/>
175+
<protectedslots title=""/>
176+
<privateslots title=""/>
177+
<events title=""/>
178+
<properties title=""/>
179+
<friends title=""/>
180+
</memberdef>
181+
<authorsection visible="yes"/>
182+
</group>
183+
184+
<!-- Layout definition for a directory page -->
185+
<directory>
186+
<briefdescription visible="yes"/>
187+
<directorygraph visible="yes"/>
188+
<memberdecl>
189+
<dirs visible="yes"/>
190+
<files visible="yes"/>
191+
</memberdecl>
192+
<detaileddescription title=""/>
193+
</directory>
194+
</doxygenlayout>

‎doc/doxygen-root/Makefile

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
default: markdown doc api adr assets cprover-manual man
2+
3+
markdown:
4+
cd .. && bash doxygen-root/doxygen-markdown/markdown.sh
5+
6+
doc:
7+
doxygen doxyfile
8+
9+
api:
10+
cd ../API && doxygen ../doxygen-root/doxyfile-doc-api
11+
mkdir -p html/api
12+
cp -r api/html/* html/api
13+
14+
adr:
15+
cd ../ADR && doxygen ../doxygen-root/doxyfile-doc-adr
16+
mkdir -p html/adr
17+
cp -r adr/html/* html/adr
18+
19+
assets:
20+
cd ../assets && doxygen ../doxygen-root/doxyfile-doc-assets
21+
mkdir -p html/assets
22+
cp -r assets/html/* html/assets
23+
cp ../assets/*.png html/assets
24+
25+
cprover-manual:
26+
cd ../cprover-manual && doxygen ../doxygen-root/doxyfile-doc-cprover-manual
27+
mkdir -p html/cprover-manual
28+
cp -r cprover-manual/html/* html/cprover-manual
29+
cp ../cprover-manual/*.c html/cprover-manual
30+
31+
man:
32+
mkdir -p html/man
33+
for man in ../man/*.1; do pandoc $$man > html/man/$$(basename $$man .1).html; done
34+
35+
36+
clean:
37+
$(RM) -r api adr assets html cprover-manual man
38+
39+
.PHONY: markdown doc api adr assets cprover-manual man clean

‎doc/doxygen-root/README.md

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
# CBMC documentation
2+
3+
This is the root of CBMC documentation.
4+
5+
## Install doxygen
6+
7+
Building this documentation requires `doxygen` and `graphviz`.
8+
9+
* On MacOS,
10+
we recommend installing with [brew](https://brew.sh/):
11+
```
12+
brew install doxygen graphviz
13+
```
14+
* On Ubuntu, we recommend installing with using `apt`:
15+
```
16+
sudo apt install doxygen graphviz
17+
```
18+
19+
Note: As of
20+
21+
## Build the documentation
22+
23+
To build the documentation, run
24+
25+
```
26+
doxygen
27+
```
28+
29+
The documentation takes about five minutes to build and is written to
30+
the `html` subdirectory as a set of 2600+ html files. To view the
31+
documentation,
32+
open the file `html/index.html` in a web browser. One MacOS, run
33+
34+
```
35+
open html/index.html
36+
```
37+
38+
## Publish the documentation
39+
40+
To publish the documentation, we use the GitHub workflow
41+
[publish.yaml](../../.github/workflow/publish.yaml) that
42+
publishes the contents of the `html` subdirectory to
43+
the `github.io` web site.
44+
45+
## Contribute documentation
46+
47+
Coming soon...
48+
49+
## References
50+
51+
* The cprover documentation: http://cprover.diffblue.com/
52+
* Sources: https://github.com/diffblue/cbmc/tree/develop/doc
53+
54+
* The cprover manual: http://www.cprover.org/cprover-manual/
55+
* Sources: https://github.com/diffblue/cbmc/tree/develop/doc/cprover-manual
56+
57+
* Doxygen manual: https://www.doxygen.nl/manual
58+
* Grouping documentation: https://www.doxygen.nl/manual/grouping.html
59+
* Markdown support: https://doxygen.nl/manual/markdown.html
60+
* Doxygen treatment of markdown pages: https://doxygen.nl/manual/markdown.html#markdown_dox

‎doc/doxygen-root/contributing.md

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
\page contributing_documentation Contributing documentation
2+
3+
The CBMC documentation is a work in progress. The quality of the
4+
documentation depends on contributions from users and developers.
5+
6+
Every markdown file in the repository contributes a page to the
7+
doxygen output. By default, a page will appear at the top-level
8+
of the tree view of the documentation on the left side of every page
9+
produced by doxygen. You can use the `\page` and `\subpage` doxygen
10+
commands to control where a page appears in this tree view.
11+
12+
If you want `child.md` to appear as a subpage of `parent.md` in the
13+
documentation, you can add
14+
```
15+
\page child Child Page Title
16+
```
17+
to the top of `child.md` and add
18+
```
19+
\subpage child
20+
```
21+
at the appropriate place in `parent.md`. The `\subpage` command will
22+
have the effect of creating a link named "Child Page Title" to
23+
`child.md` in `parent.md`. In other places (and other files),
24+
you can generate a link to `child.md` with `\ref child "link text"`.
25+
The "link text" defaults to "Child Page Title".
26+
27+
When you contribute a module `mymodule.c` to the source code, there are
28+
probably at least two kinds of documentation you want to contribute.
29+
One is user documentation to help people use your feature. One is
30+
developer documentation to help people debug or extend your work. We
31+
recommend that you put files `mymodule-user.md` and `mymodule-developer.md`
32+
next to `mymodule.c` in the repository. Then you can use the `\page`
33+
and `\subpage` mechanism described above into the appropriate parts of
34+
the user guide and developer guide.
35+
36+
When you contribute documentation, it may not be clear whether it should
37+
go into the user guide or the developer guide. We recommend that you
38+
put into the user guide everything a user needs to know to use the tool.
39+
For example, put a description of the CBMC memory model into the
40+
user guide. Then the developer guide can link to that description of the
41+
memory model in the user guide, and say, "This is the memory model, and
42+
this is how we implement the memory model."

‎doc/doxygen-root/developer_guide.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
\page developer_guide Developer guide
2+
3+
This is a CBMC developr guide.
4+
5+
* \ref cprover_documentation
6+
* [CProver Architecture Decision Records](adr/index.html)
7+
* [CProver APIs](api/index.html)
8+
* [CProver assets](assets/index.html)
9+
10+
* \ref tutorial "CProver developer tutorial"
11+
12+
This CBMC developer guide is a work in progress.
13+
Please \ref contributing_documentation "contribute documentation" and help
14+
us improve this developer guide.

0 commit comments

Comments
 (0)