Skip to content

Commit 3108086

Browse files
author
Mark R. Tuttle
committed
Elaborate content of top-level documentation pages
1 parent e73fcbb commit 3108086

File tree

5 files changed

+93
-29
lines changed

5 files changed

+93
-29
lines changed

‎doc/doxygen-root/developer_guide.md‎

Lines changed: 24 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,30 @@
1-
\page developer_guide Developer guide
1+
\page developer_guide Developer Guide
22

3-
This is a CBMC developr guide.
3+
For a quick start on developing for CBMC, read
4+
5+
* A \ref tutorial "short developer tutorial"
6+
7+
The traditional developer documentation is generated by doxygen
8+
from the source code:
49

510
* \ref cprover_documentation
11+
12+
Key concepts:
13+
14+
* \ref compilation-and-development "Compiling and developing" for CBMC
15+
* \ref background-concepts "Background concepts" including
16+
ASTs, CFGs, and SSA, bounded model checking, and static analysis
17+
* \ref goto-programs "Goto programs"
18+
* \ref goto-symex "Symbolic execution"
19+
* \ref solvers "Decision procedures"
20+
* \ref folder-walkthrough "Code organization"
21+
* [CPROVER primitives](api/index.html)
22+
23+
Miscellaneous documentation:
24+
625
* [CProver Architecture Decision Records](adr/index.html)
7-
* [CProver APIs](api/index.html)
826
* [CProver Assets](assets/index.html)
927

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.
28+
Please \ref contributing_documentation "contribute documentation"
29+
when you find mistakes or missing information to help us improve this
30+
developer guide.

‎doc/doxygen-root/index.md‎

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,35 @@
11
# Documentation
22

3-
* \subpage installation
4-
* \subpage user_guide
5-
* \subpage reference_guide
6-
* \subpage developer_guide
3+
[CBMC](https://github.com/diffblue/cbmc) is a model checker for
4+
C. This means that CBMC will explore all possible paths through your
5+
code on all possible inputs, and will check that all assertions in
6+
your code are true. CBMC can also check for the possibility of memory
7+
safety errors (like buffer overflow) and for instances of undefined
8+
behavior (like signed integer overflow). CBMC is a *bounded* model
9+
checker, however, and using CBMC may require restricting inputs to
10+
inputs of some bounded size. The result is assurance that your code
11+
behaves as expected for all such inputs.
12+
13+
This page is the root of all documentation for CBMC:
14+
15+
* The \subpage installation_guide describes how to install CBMC
16+
* The \subpage user_guide describes what you need to know to use CBMC
17+
* The \subpage reference_guide describes the CBMC tools
18+
* The \subpage developer_guide describes what you need to know to contribute
19+
to CBMC
20+
21+
CBMC documentation has traditionally been generated from
22+
doxygen comments in the source code and a few additional markdown files.
23+
Over time, we will move this documentation into the guides listed above,
24+
but for now, this source code documentation is avilable here:
725

826
* \subpage cprover_documentation
27+
28+
CBMC documentation will never be done. If you learn something interesting
29+
or find a mistake, please consider contributing documentation with a
30+
[pull request](https://github.com/diffblue/cbmc/pulls)
31+
or describing the problem to us by filing an
32+
[issue](https://github.com/diffblue/cbmc/issues).
33+
Some advice on contributing documentation is available here:
34+
935
* \subpage contributing_documentation

‎doc/doxygen-root/installation.md‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1-
\page installation Installation
1+
\page installation_guide Installation Guide
22

3-
CBMC installation instructions are on the [CBMC release page](https://github.com/diffblue/cbmc/releases/latest).
3+
The [CBMC release page](https://github.com/diffblue/cbmc/releases/latest)
4+
gives instructions for installing CBMC on MacOS, Ubuntu, Windows, and
5+
Docker.

‎doc/doxygen-root/reference_guide.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
\page reference_guide Reference guide
1+
\page reference_guide Reference Guide
22

3-
Man pages for CBMC tools:
3+
These are the man pages for the CBMC tools:
44

55
* [cbmc](man/cbmc.html)
66
* [crangler](man/crangler.html)

‎doc/doxygen-root/user_guide.md‎

Lines changed: 33 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,42 @@
1-
\page user_guide User guide
1+
\page user_guide User Guide
22

3-
This is a CBMC user guide.
3+
For a quick start with CBMC on simple problems, read
44

5-
* [CProver manual](cprover-manual/index.html)
6-
* [CProver tutorial](cprover-manual/md_cbmc-tutorial.html)
7-
* [Training material](https://model-checking.github.io/cbmc-training)
5+
* The \ref installation_guide
6+
* A [short tutorial](cprover-manual/md_cbmc-tutorial.html)
7+
* A [short manual](cprover-manual/index.html)
88

9-
Tools:
9+
For a quick start with CBMC on large software projects, read
10+
11+
* [Deploying CBMC on industrial software projects](https://model-checking.github.io/cbmc-training)
12+
describing how to use CBMC as part of routine software development and
13+
continuous integration.
14+
15+
Two third-party tools simplify using CBMC:
1016

1117
* [CBMC Viewer](https://model-checking.github.io/cbmc-viewer)
18+
scans the output of CBMC and produces a browsable summary of its findings.
1219
* [CBMC Starter Kit](https://model-checking.github.io/cbmc-starter-kit)
20+
makes it easy to add CBMC verification to an existing software project.
1321

14-
Other tips for using CBMC:
22+
Key concepts:
1523

16-
* \ref memory-analyzer
17-
* \ref memory-bounds-checking
18-
* \ref satabs
24+
* The \ref reference_guide describes CBMC and the CBMC tool chain
25+
* CBMC [primitives](cprover-manual/md_api.html) and
26+
[memory primitives](cprover-manual/md_memory-primitives.html)
27+
are useful when writing CBMC assumptions and CBMC assertions.
28+
* \ref goto-programs "goto programs" are the intermediate representation
29+
of C code used by the CBMC tool chain
30+
* \ref goto-cc "goto-cc" ([man page](man/goto-cc.html))
31+
compiles C into the goto program used by CBMC.
32+
It is intended to be a drop-in replacement for `gcc` and `cl`.
33+
* \ref goto-instrument "goto-instrument" ([man page](man/goto-instrument.html))
34+
is a collection of tools for
35+
modifying goto programs. One example is unwinding loops in a goto program.
36+
* \ref goto-analyzer "goto-analyser" ([man page](man/goto-analyzer.html))
37+
is a collection of tools for analyzing goto programs.
38+
One example is finding the set of reachable functions in a goto program.
1939

20-
This CBMC user guide is a work in progress.
21-
Please \ref contributing_documentation "contribute documentation" and help
22-
us improve this user guide.
40+
Please \ref contributing_documentation "contribute documentation"
41+
when you find mistakes or missing information to help us improve this
42+
user guide.

0 commit comments

Comments
 (0)