Improve developer documentation v2

doc/architectural/background-concepts.md

@@ -3,30 +3,30 @@
 
 \author Martin Brain, Peter Schrammel
 
-# Representations #
+\section representations_section Representations
 
-## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
+\subsection AST_section AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables
 
 To be documented.
 
-## CFG ##
+\subsection CFG_section CFG
 
 To be documented.
 
-## SSA ##
+\subsection SSA_section SSA
 
 To be documented.
 
-# Analysis techniques #
+\section analysis_techniques_section Analysis techniques
 
-## Bounded model checking ##
+\subsection BMC_section Bounded model checking
 
 To be documented (can copy from the CBMC manual).
 
-## SAT and SMT ##
+\subsection SAT_section SAT and SMT
 
 To be documented.
 
-## Static analysis ##
+\subsection static_analysis_section Static analysis
 
 To be documented.

doc/architectural/cbmc-architecture.md

@@ -52,7 +52,7 @@ be output to files (this is what `goto-cc` does) and are (informally)
 referred to as “goto binaries” or “goto programs”. The back-end are
 tools process this format, either directly from the front-end or from
 it’s saved output. These include a wide range of analysis and
-transformation tools (see \ref section-other-tools).
+transformation tools (see \ref other-tools).
 
 # Concepts #
 ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##

doc/architectural/code-walkthrough.md

@@ -0,0 +1,65 @@
+\ingroup module_hidden 
+\page code-walkthrough Code Walkthrough
+
+\author Cesar Rodriguez, Owen Jones
+
+\section data-structures-core-structures-and-ast-section Data structures: core structures and AST
+
+The core structures used for representing abstract syntax trees are all
+documented in \ref util.
+
+\section data-structures-from-ast-to-goto-program-section Data structures: from AST to GOTO program
+
+See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt::instructiont).
+
+\section front-end-languages-generating-codet-from-multiple-languages-section Front-end languages: generating codet from multiple languages
+
+\subsection language-uit-section language_uit, language_filest, languaget classes:
+
+See \ref langapi.
+
+\subsubsection parse-section Parse
+
+See \ref language_uit::parse().
+
+\subsubsection typecheck-section Typecheck
+
+See \ref language_uit::typecheck().
+
+\subsubsection final-section Final
+
+See \ref language_uit::final().
+
+\subsection languages-c-section C
+
+See \ref ansi-c.
+
+\subsection languages-cpp-section C++
+
+See \ref cpp.
+
+\subsection languages-java-section Java bytecode
+
+See \ref java_bytecode.
+
+\section bmct-class-section Bmct class
+
+\subsection equation-section equation
+
+See \ref symex-overview.
+
+
+\section symbolic-executors-section Symbolic executors
+
+\subsection symbolic-execution-section Symbolic execution
+
+See \ref symex-overview.
+
+
+\section solvers-infrastructure-section Solvers infrastructure
+
+See \ref solvers-overview.
+
+\section  static-analysis-apis-section Static analysis APIs
+
+See \ref analyses and \ref pointer-analysis.

doc/architectural/compilation-and-development.md

@@ -24,7 +24,7 @@ To be documented.
 The regression tests are contained in the `regression/` folder.
 They are grouped into directories for each of the tools/modules.
 Each of these contains multiple directories, each of which contains
-input files and one or more`.desc` files that describe what command
+input files and one or more `.desc` files that describe what command
 to run, what output is expected and so on. There is a Perl script,
 `test.pl` that is used to invoke the tests as:
 

doc/architectural/front-page.md

@@ -68,6 +68,10 @@ you can access it <a href=
 
 ### For contributors:
 
+The following pages attempt to provide the information that a developer needs to
+work on CBMC, in a sensible order. In many cases they link to the appropriate
+class-level or module-level documentation.
+
 * \subpage compilation-and-development
 
 * \subpage background-concepts
@@ -76,34 +80,23 @@ you can access it <a href=
 
 * \subpage folder-walkthrough
 
-* \subpage data-structures-core-structures-and-ast
-
-* \subpage data-structures-from-ast-to-goto-program
-
-* \subpage front-end-languages-generating-codet-from-multiple-languages
-
-* \subpage bmct-class
-
-* \subpage symbolic-executors
-
-* \subpage solvers-infrastructure
-
-* \subpage static-analysis-apis
+* \subpage code-walkthrough
 
 * \subpage other-tools
 
-* For higher-level architectural information, each of the pages under
-  the <a href="modules.html">Modules</a>
-  link gives an overview of a directory in the CProver codebase.
-
-* If you already know exactly what you're looking for, the API reference
-  is generated from the codebase. You can search for classes and class
-  members in the search bar at top-right or use one of the links in the
-  sidebar.
-
 * The \subpage tutorial "CBMC Developer Tutorial" helps new contributors
   to CProver to get their feet wet through a series of programming
   exercises - mostly modifying goto-instrument, and thus learning to
   manipulate the main data structures used within CBMC.
 
+For higher-level architectural information, each of the pages under
+the <a href="modules.html">Modules</a>
+link gives an overview of a directory in the CProver codebase.
+
+If you already know exactly what you're looking for, the best place
+to look is the API reference, which
+is generated from the codebase. You can search for classes and class
+members in the search bar at top-right or use one of the links in the
+sidebar.
+
 \defgroup module_hidden _hidden