Skip to content

Commit 467873e

Browse files
CharliemowoodCharliemowood
committed
Assign every module a README.md
Add doxygen layout to make change modules in toc to directories Put all modules in the directories folder by specifying the correct doxygen command Remove references in code to document pages which are not required
1 parent 9565bcf commit 467873e

File tree

39 files changed

+457
-140
lines changed

39 files changed

+457
-140
lines changed

‎doc/architectural/cprover-architecture-overview.md

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,18 @@
1-
\ingroup module_hidden
21
\page cprover-architecture-overview CProver Architecture Overview
32

43
\author Martin Brain
54

65
Background Information
76
======================
87

9-
First off; read the \ref cbmc-user-manual "CBMC User-Manual". It describes
8+
First off; read the \ref cbmc-user-manual "CBMC User Manual". It describes
109
how to get, build and use CBMC. This document covers the
1110
internals of the system and how to get started on development.
1211

1312
Documentation
1413
-------------
1514

16-
Apart from the (user-orientated) CPROVER manual and this document, most
15+
Apart from the (user-orientated) CBMC user manual and this document, most
1716
of the rest of the documentation is inline in the code as `doxygen` and
1817
some comments. A man page for CBMC, goto-cc and goto-instrument is
1918
contained in the `doc/` directory and gives some options for these
@@ -602,3 +601,52 @@ they are in the code.
602601

603602
[^3]: When `USE_DSTRING` is enabled (it is by default), this is actually
604603
a `dstring` and thus an integer which is a reference into a string table
604+
605+
606+
\section cbmc-tour CBMC tour
607+
Graphical Tour of the CBMC architecture
608+
----------------------------------------
609+
610+
This section provides a graphical overview of how CBMC fits together.
611+
CBMC takes C code or a goto-binary as input and tries to emit traces
612+
of executions that lead to crashes or undefined behaviour. The diagram
613+
below shows the intermediate steps in this process.
614+
615+
616+
\dot
617+
digraph G {
618+
619+
rankdir="TB";
620+
node [shape=box, fontcolor=blue];
621+
622+
subgraph top {
623+
rank=same;
624+
1 -> 2 -> 3 -> 4;
625+
}
626+
627+
subgraph bottom {
628+
rank=same;
629+
5 -> 6 -> 7 -> 8 -> 9;
630+
}
631+
632+
/* shift bottom subgraph over */
633+
9 -> 1 [color=white];
634+
635+
4 -> 5;
636+
637+
1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
638+
2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
639+
3 [label="language\ntype-checking" URL="\ref type-checking"];
640+
4 [label="goto\nconversion" URL="\ref goto-conversion"];
641+
5 [label="instrumentation" URL="\ref instrumentation"];
642+
6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
643+
7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
644+
8 [label="decision\nprocedure" URL="\ref decision-procedure"];
645+
9 [label="counter example\nproduction" URL="\ref counter-example-production"];
646+
}
647+
\enddot
648+
649+
Next steps: the \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
650+
perspective. Each node in the diagram above links to the appropriate
651+
class or module documentation, describing that particular stage in the
652+
CBMC pipeline.

‎doc/architectural/front-page.md

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,5 +86,3 @@ module pages at the moment, but may be somewhat out-of-date.
8686
to CProver to get their feet wet through a series of programming
8787
exercises - mostly modifying goto-instrument, and thus learning to
8888
manipulate the main data structures used within CBMC.
89-
90-
\defgroup module_hidden _hidden

‎doc/cbmc-user-manual.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
\ingroup module_hidden
21
\page cbmc-user-manual CMBC User Manual
32

43
\author Daniel Kroening

‎src/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>

‎src/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,4 +106,7 @@ ipasir-build: ipasir-download
106106
$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
107107
@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
108108

109+
doc :
110+
doxygen
111+
109112
.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build

‎src/analyses/README.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
\defgroup analyses
2+
\ingroup analyses
3+
4+
FIXME: put here a good introduction describing what is contained
5+
in this folder.

‎src/ansi-c/module.md renamed to ‎src/ansi-c/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\ingroup module_hidden
2-
\defgroup module_ansi-c ANSI-C Language Front-end
1+
\defgroup ansi-c
2+
\ingroup ansi-c
33

44
\author Kareem Khazem
55

‎src/assembler/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
\defgroup assembler
2+
\ingroup assembler
3+
4+
`assembler/` is a module that serve as language front end.

‎src/big-int/README.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
\defgroup big-int
2+
\ingroup big-int
3+
4+
CPROVER is distributed with its own multi-precision arithmetic library;
5+
mainly for historical and portability reasons. The library is externally
6+
developed and thus `big-int` contains the source as it is distributed.
7+
This should not be used directly, see `util/mp_arith.h` for the CPROVER
8+
interface.

‎src/cbmc/README.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
\defgroup cbmc
2+
\ingroup cbmc
3+
4+
5+
The CBMC handles the code related to interacting with CBMC.

‎src/cbmc/module.md

Lines changed: 0 additions & 47 deletions
This file was deleted.

‎src/clobber/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
\defgroup clobber
2+
\ingroup clobber
3+
4+
`clobber\` is a module that is a tool.

‎src/cpp/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
\defgroup cpp
2+
\ingroup cpp
3+
4+
The C++ Language front-end is for processing C++.

‎src/cpp/cpp_language.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_CPP_CPP_LANGUAGE_H
1313
#define CPROVER_CPP_CPP_LANGUAGE_H
1414

15-
/*! \defgroup gr_cpp C++ front-end */
16-
1715
#include <memory>
1816

1917
#include <util/make_unique.h> // unique_ptr

‎src/doxyfile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -684,7 +684,7 @@ FILE_VERSION_FILTER =
684684
# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE
685685
# tag is left empty.
686686

687-
LAYOUT_FILE =
687+
LAYOUT_FILE = DoxygenLayout.xml
688688

689689
# The CITE_BIB_FILES tag can be used to specify one or more bib files containing
690690
# the reference definitions. This must be a list of .bib files. The .bib

0 commit comments

Comments
 (0)