Elaborate content of top-level documentation pages

doc/doxygen-root/developer_guide.md

@@ -1,14 +1,30 @@
-\page developer_guide Developer guide
+\page developer_guide Developer Guide
 
-This is a CBMC developr guide.
+For a quick start on developing for CBMC, read
+
+* A \ref tutorial "short developer tutorial"
+
+The traditional developer documentation is generated by doxygen
+from the source code:
 
 * \ref cprover_documentation
+
+Key concepts:
+
+  * \ref compilation-and-development "Compiling and developing" for CBMC
+  * \ref background-concepts "Background concepts" including
+  ASTs, CFGs, and SSA, bounded model checking, and static analysis
+  * \ref goto-programs "Goto programs"
+  * \ref goto-symex "Symbolic execution"
+  * \ref solvers "Decision procedures"
+  * \ref folder-walkthrough "Code organization"
+  * [CPROVER primitives](api/index.html)
+
+Miscellaneous documentation:
+
   * [CProver Architecture Decision Records](adr/index.html)
-  * [CProver APIs](api/index.html)
   * [CProver Assets](assets/index.html)
 
-* \ref tutorial "CProver developer tutorial"
-
-This CBMC developer guide is a work in progress.
-Please \ref contributing_documentation "contribute documentation" and help
-us improve this developer guide.
+Please \ref contributing_documentation "contribute documentation"
+when you find mistakes or missing information to help us improve this
+developer guide.

doc/doxygen-root/index.md

@@ -1,9 +1,35 @@
 # Documentation
 
-* \subpage installation
-* \subpage user_guide
-* \subpage reference_guide
-* \subpage developer_guide
+[CBMC](https://github.com/diffblue/cbmc) is a model checker for
+C. This means that CBMC will explore all possible paths through your
+code on all possible inputs, and will check that all assertions in
+your code are true. CBMC can also check for the possibility of memory
+safety errors (like buffer overflow) and for instances of undefined
+behavior (like signed integer overflow). CBMC is a *bounded* model
+checker, however, and using CBMC may require restricting inputs to
+inputs of some bounded size. The result is assurance that your code
+behaves as expected for all such inputs.
+
+This page is the root of all documentation for CBMC:
+
+* The \subpage installation_guide describes how to install CBMC
+* The \subpage user_guide describes what you need to know to use CBMC
+* The \subpage reference_guide describes the CBMC tools
+* The \subpage developer_guide describes what you need to know to contribute
+  to CBMC
+
+CBMC documentation has traditionally been generated from
+doxygen comments in the source code and a few additional markdown files.
+Over time, we will move this documentation into the guides listed above,
+but for now, this source code documentation is avilable here:
 
 * \subpage cprover_documentation
+
+CBMC documentation will never be done.  If you learn something interesting
+or find a mistake, please consider contributing documentation with a
+[pull request](https://github.com/diffblue/cbmc/pulls)
+or describing the problem to us by filing an
+[issue](https://github.com/diffblue/cbmc/issues).
+Some advice on contributing documentation is available here:
+
 * \subpage contributing_documentation

doc/doxygen-root/installation.md

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

doc/doxygen-root/reference_guide.md

@@ -1,6 +1,6 @@
-\page reference_guide Reference guide
+\page reference_guide Reference Guide
 
-Man pages for CBMC tools:
+These are the man pages for the CBMC tools:
 
 * [cbmc](man/cbmc.html)
 * [crangler](man/crangler.html)

doc/doxygen-root/user_guide.md

@@ -1,22 +1,42 @@
-\page user_guide User guide
+\page user_guide User Guide
 
-This is a CBMC user guide.
+For a quick start with CBMC on simple problems, read
 
-* [CProver manual](cprover-manual/index.html)
-* [CProver tutorial](cprover-manual/md_cbmc-tutorial.html)
-* [Training material](https://model-checking.github.io/cbmc-training)
+* The \ref installation_guide
+* A [short tutorial](cprover-manual/md_cbmc-tutorial.html)
+* A [short manual](cprover-manual/index.html)
 
-Tools:
+For a quick start with CBMC on large software projects, read
+
+* [Deploying CBMC on industrial software projects](https://model-checking.github.io/cbmc-training)
+  describing how to use CBMC as part of routine software development and
+  continuous integration.
+
+Two third-party tools simplify using CBMC:
 
 * [CBMC Viewer](https://model-checking.github.io/cbmc-viewer)
+  scans the output of CBMC and produces a browsable summary of its findings.
 * [CBMC Starter Kit](https://model-checking.github.io/cbmc-starter-kit)
+  makes it easy to add CBMC verification to an existing software project.
 
-Other tips for using CBMC:
+Key concepts:
 
-* \ref memory-analyzer
-* \ref memory-bounds-checking
-* \ref satabs
+* The \ref reference_guide describes CBMC and the CBMC tool chain
+* CBMC [primitives](cprover-manual/md_api.html) and
+  [memory primitives](cprover-manual/md_memory-primitives.html)
+  are useful when writing CBMC assumptions and CBMC assertions.
+* \ref goto-programs "goto programs" are the intermediate representation
+  of C code used by the CBMC tool chain
+* \ref goto-cc "goto-cc" ([man page](man/goto-cc.html))
+  compiles C into the goto program used by CBMC.
+  It is intended to be a drop-in replacement for `gcc` and `cl`.
+* \ref goto-instrument "goto-instrument" ([man page](man/goto-instrument.html))
+  is a collection of tools for
+  modifying goto programs.  One example is unwinding loops in a goto program.
+* \ref goto-analyzer "goto-analyser" ([man page](man/goto-analyzer.html))
+  is a collection of tools for analyzing goto programs.
+  One example is finding the set of reachable functions in a goto program.
 
-This CBMC user guide is a work in progress.
-Please \ref contributing_documentation "contribute documentation" and help
-us improve this user guide.
+Please \ref contributing_documentation "contribute documentation"
+when you find mistakes or missing information to help us improve this
+user guide.