Merge pull request #7874 from martin-cs/fix/documentation-tidy

A couple of minor documentation fixes

Author: martin-cs

src/analyses/README.md

@@ -69,7 +69,7 @@ apply the dominator algorithm to its Java bytecode representation.
 `cfg_dominators_templatet::output` is a good place to check how to query the
 dominators it has found.
 
-\subsection analyses-constant-propagation Constant propagation (\ref constant_propagator_ait)
+\subsection analyses-constant-propagation Constant propagation (constant_propagator_ait)
 
 A simple, unsound constant propagator. Replaces RHS symbol expressions (variable
 reads) with their values when they appear to have a unique value at a particular
@@ -242,10 +242,6 @@ To be documented.
 
 \section analyses-transformations Transformations (arguably in the wrong directory):
 
-\subsection analyses-goto-checkt Pointer / overflow / other check insertion (goto_checkt)
-
-To be documented.
-
 \subsection analyses-interval-analysis Integer interval analysis -- both an analysis and a transformation
 
 \ref interval_analysis interprets instructions of the input \ref goto_modelt

src/goto-instrument/contracts/doc/user/contracts-loops.md

@@ -4,7 +4,7 @@ Back to @ref contracts-user
 
 @tableofcontents
 
-CBMC offers support for loop contracts, which includes three basic clauses:
+CBMC offers support for loop contracts, which includes four basic clauses:
 - an _invariant_ clause for establishing safety properties,
 - a _decreases_ clause for establishing termination,
 - an _assigns_ clause for declaring the memory locations assignable by the loop,