Some cleanup in the architecture overview doc

Author: peterschrammel

doc/architectural/cprover-architecture-overview.md

@@ -1,9 +1,99 @@
-\ingroup module_hidden 
+\ingroup module_hidden
 \page cprover-architecture-overview CProver Architecture Overview
 
-\author Martin Brain
+\author Martin Brain, Peter Schrammel
 
-Background Information
+# Overview of CPROVER Directories
+
+`src/`
+------
+
+The source code is divided into a number of sub-directories, each
+containing the code for a different part of the system. In the top level
+files there are only a few files:
+
+* `config.inc`:   The user-editable configuration parameters for the
+  build process. The main use of this file is setting the paths for the
+  various external SAT solvers that are used. As such, anyone building
+  from source will likely need to edit this.
+
+* `Makefile`:   The main systems Make file. Parallel builds are
+  supported and encouraged; please don’t break them!
+
+* `common`:   System specific magic required to get the system to build.
+  This should only need to be edited if porting CBMC to a new platform /
+  build environment.
+
+* `doxygen.cfg`:   The config file for doxygen.cfg
+
+
+- GOTO-Programs
+
+  * \ref goto-programs
+  * \ref linking
+
+- Symbolic Execution
+  * \ref goto-symex
+
+- Static Analyses
+
+  * \ref analyses
+  * \ref pointer-analysis
+
+- Solvers
+  * \ref solvers
+
+- Language Front Ends
+
+  * Language API: \ref langapi
+  * C: \ref ansi-c
+  * C++: \ref cpp
+  * Java: \ref java_bytecode
+  * JavaScript: \ref jsil
+
+- Tools
+
+  * \ref cbmc
+  * \ref clobber
+  * \ref goto-analyzer
+  * \ref goto-instrument
+  * \ref goto-diff
+  * \ref memory-models
+  * \ref goto-cc
+  * \ref jbmc
+
+- Utilities
+
+  * \ref big-int
+  * \ref json
+  * \ref xmllang
+  * \ref util
+  * \ref miniz
+  * \ref nonstd
+
+
+`doc`
+-----
+
+Contains the CBMC man page. Doxygen HTML pages are generated
+into the `doc/html` directory when running `doxygen` from `src`.
+
+`regression/`
+-------------
+
+The `regression/` directory contains the test suites.
+They are grouped into directories for each of the tools/modules.
+Each of these contains a directory per test case, containing a C or C++
+file that triggers the bug and a `.desc` file that describes
+the tests, expected output and so on. There is a Perl script,
+`test.pl` that is used to invoke the tests as:
+
+    ../test.pl -c PATH_TO_CBMC
+
+The `–help` option gives instructions for use and the
+format of the description files.
+
+General Information
 ======================
 
 First off; read the \ref cbmc-user-manual "CBMC User Manual". It describes
@@ -35,16 +125,21 @@ transformation tools (see Section \ref other-apps "Other apps").
 Coding Standards
 ----------------
 
+See [CODING_STANDARD](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md).
+
 CPROVER is written in a fairly minimalist subset of C++; templates and
-meta-programming are avoided except where necessary. The standard
-library is used but in many cases there are alternatives provided in
-`util/` (see Section \ref util-section Util ) which are preferred.  Boost is
-not used.
+meta-programming are avoided except where necessary.
+External library dependencies are avoided (only STL and a SAT solver
+are required). Boost is not used. The `util` directory contains many
+utilities that are not (yet) in the standard library.
 
 Patches should be formatted so that code is indented with two space
-characters, not tab and wrapped to 75 or 72 columns. Headers for doxygen
+characters, not tab and wrapped to 80 columns. Headers for doxygen
 should be given (and preferably filled!) and the author will be the
-person who first created the file.
+person who first created the file. Add doxygen comments to
+undocumented functions as you touch them. Coding standards
+and doxygen comments are enforced by CI before a patch can be
+merged by running `clang-format` and `cpplint`.
 
 Identifiers should be lower case with underscores to separate words.
 Types (classes, structures and typedefs) names must[^1] end with a `t`.
@@ -53,61 +148,12 @@ interpreted) are named with `_typet`. For example `ui_message_handlert`
 rather than `UI_message_handlert` or `UIMessageHandler` and
 `union_typet`.
 
-# Overview of CPROVER directories
-
-- language front ends
-
-  * \ref ansi-c
-  * \ref cpp
-  * \ref langapi
-  * \ref jsil
-
-
-- static analysis
-
-  * \ref analyses
-  * \ref pointer-analysis
-
-
-- utilities
-
-  * \ref big-int
-  * \ref json
-  * \ref xmllang
-  * \ref util
-  * \ref miniz
-  * \ref nonstd
-
-
-- tools
-
-  * \ref cbmc
-  * \ref clobber
-  * \ref goto-analyzer
-  * \ref goto-instrument
-  * \ref goto-diff
-  * \ref memory-models
-  * \ref goto-cc
-  * \ref jbmc
-
-
-- goto-programs
-
-  * \ref goto-programs
-  * \ref linking
-
-
-- symbolic execution
-   * \ref goto-symex
-
-
-- solvers
-  * \ref solvers
-
-\section other-apps Other apps
+\section other-apps Other Tools
 Other Useful Code
 -----------------
 
+FIXME: The text in this section is a bit outdated.
+
 The CPROVER subversion archive contains a number of separate programs.
 Others are developed separately as patches or separate
 branches.Interfaces are have been and are continuing to stablise but
@@ -187,48 +233,6 @@ Source Walkthrough
 This section walks through the code bases in a rough order of interest /
 comprehensibility to the new developer.
 
-`doc`
------
-
-At the moment just contains the CBMC man page.
-
-`regression/`
--------------
-
-The regression tests are currently being moved from CVS. The
-`regression/` directory contains all of those that have
-been moved. They are grouped into directories for each of the tools.
-Each of these contains a directory per test case, containing a C or C++
-file that triggers the bug and a `.dsc` file that describes
-the tests, expected output and so on. There is a Perl script,
-`test.pl` that is used to invoke the tests as:
-
-    ../test.pl -c PATH_TO_CBMC
-
-The `–help` option gives instructions for use and the
-format of the description files.
-
-`src/`
-------
-
-The source code is divided into a number of sub-directories, each
-containing the code for a different part of the system. In the top level
-files there are only a few files:
-
-* `config.inc`:   The user-editable configuration parameters for the
-  build process. The main use of this file is setting the paths for the
-  various external SAT solvers that are used. As such, anyone building
-  from source will likely need to edit this.
-
-* `Makefile`:   The main systems Make file. Parallel builds are
-  supported and encouraged; please don’t break them!
-
-* `common`:   System specific magic required to get the system to build.
-  This should only need to be edited if porting CBMC to a new platform /
-  build environment.
-
-* `doxygen.cfg`:   The config file for doxygen.cfg
-
 \section util-section util directory
 util/
 -----------------