Improve developer documentation v2

doc/architectural/bmct-class.md

@@ -5,4 +5,4 @@
 
 ## equation ##
 
-To be documented.
+See \ref symex-overview.

doc/architectural/data-structures-from-ast-to-goto-program.md

@@ -5,35 +5,7 @@
 
 ## goto_programt ##
 
-See \ref goto_programt.
-
-### instructiont ###
-
-See [instructiont](\ref goto_programt::instructiont).
-
-#### Types, motivation of each type #####
-
-See [instructiont](\ref goto_programt::instructiont).
-
-#### Accepted code (codet) values ####
-
-To be documented.
-
-#### Accepted guard (exprt) values ####
-
-To be documented.
-
-## goto_functionst ##
-
-\ref goto_functionst is a map from function names to function bodies (CFGs).
-
-To be documented.
-
-## goto_modelt ##
-
-\ref goto_modelt is a compilation unit.
-
-To be documented.
+See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt::instructiont).
 
 ## Example: ##
 

doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md

@@ -5,24 +5,32 @@
 
 ## language_uit, language_filest, languaget classes: ##
 
-### Purpose ###
-
-To be documented.
+See \ref langapi.
 
 ### Parse ###
 
-To be documented.
+See \ref language_uit::parse().
 
 ### Typecheck ###
 
-To be documented.
+See \ref language_uit::typecheck().
 
 ### Final ###
 
-To be documented.
+See \ref language_uit::final().
+
+## C ##
+
+See \ref ansi-c.
+
+## C++ ##
+
+See \ref cpp.
 
 ## Java bytecode ##
 
+See \ref java_bytecode.
+
 ### Explain how a java program / class is represented in a .class ###
 
 To be documented.

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
@@ -92,18 +96,19 @@ you can access it <a href=
 
 * \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

doc/architectural/solvers-infrastructure.md

@@ -3,6 +3,8 @@
 
 \author
 
+See \ref solvers-overview.
+
 ## Flattening ##
 
 To be documented.

doc/architectural/static-analysis-apis.md

@@ -3,4 +3,5 @@
 
 \author 
 
-To be documented.
+
+See \ref analyses and \ref pointer-analysis.

doc/architectural/symbolic-executors.md

@@ -3,6 +3,6 @@
 
 \author 
 
-## Symex class ##
+## Symbolic execution ##
 
-To be documented.
+See \ref symex-overview.