diff --git a/doc/doxygen-root/developer_guide.md b/doc/doxygen-root/developer_guide.md index a878940fe6e..7df6952222e 100644 --- a/doc/doxygen-root/developer_guide.md +++ b/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. diff --git a/doc/doxygen-root/index.md b/doc/doxygen-root/index.md index b0990342a03..e96704ec1fe 100644 --- a/doc/doxygen-root/index.md +++ b/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 diff --git a/doc/doxygen-root/installation.md b/doc/doxygen-root/installation.md index 82567967f9c..802c811a291 100644 --- a/doc/doxygen-root/installation.md +++ b/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. diff --git a/doc/doxygen-root/reference_guide.md b/doc/doxygen-root/reference_guide.md index d3efb2e66c4..3633e41e156 100644 --- a/doc/doxygen-root/reference_guide.md +++ b/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) diff --git a/doc/doxygen-root/user_guide.md b/doc/doxygen-root/user_guide.md index cea3eb5f19b..6f0ec6aa366 100644 --- a/doc/doxygen-root/user_guide.md +++ b/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.