Update docs for goto-programs

Author: smowton

src/goto-programs/README.md

@@ -124,8 +124,12 @@ digraph G {
 }
 \enddot
 
-At this stage, CBMC constructs a goto-program from a symbol table. It
-does not use the parse tree or the source file at all for this step. This
+At this stage, CBMC constructs a goto-program from a symbol table.
+Each symbol in the symbol table with function type (that is, the symbol's `type`
+field contains a \ref code_typet) will be converted to a corresponding GOTO
+program.
+
+It does not use the parse tree or the source file at all for this step. This
 may seem surprising, because the symbols are stored in a hash table and
 therefore have no intrinsic order; nevertheless, every \ref symbolt is
 associated with a \ref source_locationt, allowing CBMC to figure out the
@@ -282,18 +286,6 @@ This is not the final form of the goto-functions, since the lists of
 instructions will be 'normalized' in the next step (Instrumentation),
 which removes some instructions and adds targets to others.
 
-Note that goto_programt and goto_functionst are each template
-instantiations; they are currently the *only* specialization of
-goto_program_templatet and goto_functions_templatet, respectively. This
-means that the generated Doxygen documentation can be somewhat obtuse
-about the actual types of things, and is unable to generate links to the
-correct classes. Note that the
-\ref goto_programt::instructiont::code "code" member of a
-goto_programt's instruction has type \ref codet (its type in the
-goto_program_templatet documentation is given as "codeT", as this is the
-name of the template's type parameter); similarly, the type of a guard
-of an instruction is \ref guardt.
-
 ---
 \section instrumentation Instrumentation
 
@@ -324,8 +316,15 @@ previous stage:
   are littered with \ref code_skipt "skip" statements. The
   instrumentation stage removes the majority of these.
 
-* Function pointers are removed. They are turned into switch statements
-  (but see the next point; switch statements are further transformed).
+* Variable lifespan implied by \ref code_declt instructions and lexical scopes
+  described by \ref code_blockt nodes is replaced by `DECL` and corresponding
+  `DEAD` instructions. There are therefore no lexical scopes in GOTO programs
+  (not even local variable death on function exit is enforced).
+
+* Expressions with side-effects are explicitly ordered so that there is one
+  effect per instruction (apart from function call instructions, which can
+  still have many). For example, `y = f() + x++` will have become something like
+  `tmp1 = f(); y = tmp1 + x; x = x + 1;`
 
 * Compound blocks are eliminated. There are several subclasses of
   \ref codet that count as 'compound blocks;' therefore, later stages in
@@ -362,13 +361,7 @@ previous stage:
 * \ref code_returnt "return statements" are transformed into
   (unconditional) GOTOs whose target is the \ref END_FUNCTION
   instruction. Each goto_programt should have precisely one such
-  instruction. Note the presence of \ref code_deadt, which has a
-  \ref code_deadt::symbol() "symbol()" member. Deads mark symbols that
-  have just gone out of scope; typically, a GOTO that jumps to an
-  END_FUNCTION instruction is preceded by a series of deads. Deads also
-  follow sequences of instructions that were part of the body of a
-  block (loop, conditional etc.) if there were symbols declared in that
-  block.
+  instruction.
 
 This stage concludes the *analysis-independent* program transformations.