Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation

Minor fixes to documentation outline

Author: tautschnig

doc/architectural/background-concepts.md

@@ -13,15 +13,15 @@ To be documented.
 
 To be documented.
 
-### SSA ###
+## SSA ##
 
 To be documented.
 
 # Analysis techniques #
 
-## Bounded model checking (from the CBMC manual) ##
+## Bounded model checking ##
 
-To be documented.
+To be documented (can copy from the CBMC manual).
 
 ## SAT and SMT ##
 

doc/architectural/cbmc-architecture.md

@@ -55,30 +55,28 @@ it’s saved output. These include a wide range of analysis and
 transformation tools (see \ref section-other-tools).
 
 # Concepts #
-## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
+## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
 
 To be documented.
 
-## Instrumentation (for test gen & CBMC & ...): Goto functions -> goto functions ##
+## Instrumentation: goto functions → goto functions ##
 
 To be documented.
 
-## Goto functions -> BMC -> Counterexample (trace) ##
+## Goto functions → BMC → Counterexample (trace) ##
 
 To be documented.
 
-## Trace -> interpreter -> memory map ##
+## Trace → interpreter → memory map ##
 
 To be documented.
 
-## Goto functions -> abstract interpretation ##
+## Goto functions → abstract interpretation ##
 
 To be documented.
 
 ## Executables (flow of transformations): ##
 
-To be documented.
-
 ### goto-cc ###
 
 To be documented.

doc/architectural/data-structures-core-structures-and-ast.md

@@ -87,19 +87,16 @@ To be documented.
 
 To be documented.
 
-
 ## Examples: how to represent the AST of statements, in C and in java ##
 
-To be documented.
-
-### struct Array { int length, int *data }; ###
+### x = y + 123 ###
 
-To be documented.
+To be documented..
 
-### x = y + 123 ###
+### if (x > 10) { y = 2 } else { v[3] = 4 } ###
 
 To be documented.
 
-### if (x > 10) { y = 2 } else { v[3] = 4 } ###
+### Java arrays: struct Array { int length, int *data }; ###
 
 To be documented.

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

@@ -5,19 +5,15 @@
 
 ## goto_programt ##
 
-To be documented.
-
-### The CFG of a function ###
-
-To be documented.
+See \ref goto_programt.
 
 ### instructiont ###
 
-See documentation at \ref instructiont.
+See [instructiont](\ref goto_programt::instructiont).
 
-#### Types, motivation of each type (dead?) #####
+#### Types, motivation of each type #####
 
-To be documented.
+See [instructiont](\ref goto_programt::instructiont).
 
 #### Accepted code (codet) values ####
 
@@ -29,24 +25,18 @@ To be documented.
 
 ## goto_functionst ##
 
-To be documented.
-
-### A map from function names to function bodies (CFGs) ###
+\ref goto_functionst is a map from function names to function bodies (CFGs).
 
 To be documented.
 
 ## goto_modelt ##
 
-To be documented.
-
-### A compilation unit ###
+\ref goto_modelt is a compilation unit.
 
 To be documented.
 
 ## Example: ##
 
-To be documented.
-
 ### Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } ###
 
 To be documented.

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

@@ -3,13 +3,7 @@
 
 \author Martin Brain, Peter Schrammel
 
-## Front-end languages: generating codet from multiple languages ##
-
-To be documented.
-
-### language_uit, language_filest, languaget classes: ###
-
-To be documented.
+## language_uit, language_filest, languaget classes: ##
 
 ### Purpose ###
 
@@ -27,14 +21,16 @@ To be documented.
 
 To be documented.
 
-## Java bytecode: ##
+## Java bytecode ##
+
+### Explain how a java program / class is represented in a .class ###
 
 To be documented.
 
-### Explain how a java program / class is represented in a .class ###
+### Explain the 2 step conversion from bytecode to codet ###
 
 To be documented.
 
-### Explain the 2 step conversion from bytecode to codet; give an example with a class? ###
+### A worked example of converting java bytecode to codet ###
 
 To be documented.