Merge pull request #6982 from tautschnig/cleanup/cprover-manual

Cleanup CPROVER Manual

Author: tautschnig

doc/cprover-manual/api.md

@@ -31,7 +31,7 @@ The functions **\_\_CPROVER\_input** and **\_\_CPROVER\_output** are
 used to report an input or output value. Note that they do not generate
 input or output values. The first argument is a string constant to
 distinguish multiple inputs and outputs (inputs are typically generated
-using nondeterminism, as described [here](./modeling-nondeterminism.md)). The
+using nondeterminism, as described [here](../modeling/nondeterminism/)). The
 string constant is followed by an arbitrary number of values of
 arbitrary types.
 
@@ -159,12 +159,12 @@ int main()
 
 #### Uninterpreted Functions
 
-Uninterpreted functions are documented [here](./modeling-nondeterminism.md)).
+Uninterpreted functions are documented [here](../modeling/nondeterminism/)).
 
 ### Memory-Related Functions
 
 The semantics of the primitives listed in this section is described in more detail in the
-document about [Memory Primitives](http://cprover.diffblue.com/memory-primitives.html).
+document about [Memory Primitives](../memory-primitives/).
 
 #### \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_same\_object
 
@@ -184,7 +184,7 @@ arguments point to the same object.
 
 The following primitives require a pointer that is null or valid in order to
 have well-defined semantics in all usage cases. See the document about
-[Memory Primitives](http://cprover.diffblue.com/memory-primitives.html)
+[Memory Primitives](../memory-primitives/)
 for more details. It also includes a description of the `--pointer-primitive-check`
 option to verify the preconditions of the primitives.
 

doc/cprover-manual/cbmc-tutorial.md

@@ -137,13 +137,6 @@ possible output format.
     cbmc file1.c --bounds-check --pointer-check --trace --xml-ui
 ```
 
-The specification of the XML trace output can be found here: [XML
-Specification](../assets/xml_spec.tex)
-and can be built by `pdflatex -shell-escape xml_spec.tex`. See the [README
-](../assets/README.md#xml_spec.tex) for details.
-
-Alternatively, you can view it in [Markdown](../assets/xml_spec.md).
-
 ### Verifying Modules
 
 In the example above, we used a program that starts with a `main`

doc/cprover-manual/contracts-assigns.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Assigns Clause
 
 ## In Function Contracts
@@ -135,8 +137,8 @@ where the left-hand-side is in the *free* set are not instrumented with the abov
 
 Assuming _assigns_ clauses are a sound abstraction of the write set for
 a given function, CBMC will use the function contract in place of the function
-implementation as described by [Requires \& Ensures
-Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will add
+implementation as described by
+[Requires \& Ensures Clauses](../../contracts/requires-and-ensures/#replacement), and it will add
 non-deterministic assignments for each object listed in the `__CPROVER_assigns`
 clause. Since these objects might be modified by the function, CBMC uses
 non-deterministic assignments to havoc them and restrict their values only by

doc/cprover-manual/contracts-decreases.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Decreases Clauses
 
 A _decreases_ clause specifies a measure that must strictly decrease at every iteration of a loop.
@@ -30,7 +32,7 @@ __CPROVER_decreases(n - i)
 { ... }
 ```
 
-Please see the [invariant clauses](contracts-invariants.md) page
+Please see the [invariant clauses](../../contracts/invariants/) page
 for more examples on `for` and `do...while` loops.
 
 To help prove termination of more complex loops,
@@ -69,7 +71,7 @@ Decreases clause is not side-effect free. (at: file main.c line 4 function main)
 
 ### Semantics
 
-A decreases clause extends the loop abstraction introduced in the [invariants clause](contracts-invariants.md) manual.
+A decreases clause extends the loop abstraction introduced in the [invariants clause](../../contracts/invariants/) manual.
 In addition to the inductiveness check asserted at the end of a single arbitrary iteration,
 CBMC would also assert the strict decrement of the measure specified in the decreases clause.
 At a high level, in addition to the assumptions and assertions introduced by the invariant clause,
@@ -166,7 +168,7 @@ int binary_search(int val, int *buf, int size)
 The instrumented code points (5), (6), (8), and (9) are specific to the decreases clause.
 
 **Important.** 
-Decreases clauses work in conjunction with [loop invariants](contract-invariants.md),
+Decreases clauses work in conjunction with [loop invariants](../../contracts/invariants/),
 which model an arbitrary loop iteration at which the decreases clause is checked.
 If a decreases clause is annotated on a loop without an invariant clause,
 then the weakest possible invariant (i.e, `true`) is used to model an arbitrary iteration.

doc/cprover-manual/contracts-functions.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Function Contracts
 
 CBMC offers support for function contracts, which includes three basic clauses:
@@ -56,9 +58,9 @@ A function contract has three parts:
 In our example, the developer may require from the caller to properly allocate
 all arguments, thus, pointers must be valid. We can specify the preconditions of
 a function using `__CPROVER_requires` (see [Requires \& Ensures
-Clauses](contracts-requires-and-ensures.md) Section for details) and we can
+Clauses](../../contracts/requires-and-ensures/) for details) and we can
 specify an allocated object using a predicate called `__CPROVER_is_fresh` (see
-[Memory Predicate](contracts-memory-predicates.md) Section for details). Thus, for the `sum` function, the set
+[Memory Predicate](../../contracts/memory-predicates/) for details). Thus, for the `sum` function, the set
 of preconditions are
 
 ```c
@@ -67,15 +69,15 @@ __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
 ```
 
 We can use `__CPROVER_ensures` to specify postconditions (see [Requires \&
-Ensures Clauses](contracts-requires-and-ensures.md) Section for details).  In our
+Ensures Clauses](../../contracts/requires-and-ensures/) for details).  In our
 example, developers can use the built-in construct `__CPROVER_return_value`,
 which represents the return value of a function. As postconditions, one may list
 possible return values (in this case, either `SUCCESS` or `FAILURE`) as well as
 describe the main property of this function: if the function returns `SUCCESS`,
 then `*out` stores the result of `a + b`.  We can also check that the value in
 `*out` will be preserved in case of failure by using `__CPROVER_old`, which
 refers to the value of a given object in the pre-state of a function (see
-[History Variables](contracts-history-variables.md) Section for details). Thus, for the `sum` function, the
+[History Variables](../../contracts/history-variables/) for details). Thus, for the `sum` function, the
 set of postconditions are
 
 
@@ -87,7 +89,7 @@ __CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old
 ```
 
 Finally, the _assigns_ clause allows developers to define a frame condition (see
-[Assigns Clause](contracts-assigns.md) Section for details).
+[Assigns Clause](../../contracts/assigns/) for details).
 In general, systems for describing the frame condition of a function
 use either writes or modifies semantics; this design is based on the former.
 This means that memory not specified by the assigns clause must
@@ -149,8 +151,8 @@ program using contracts.
 
 ## Additional Resources
 
-- [Requires \& Ensures Clauses](contracts-requires-and-ensures.md)
-- [Assigns Clause](contracts-assigns.md)
-- [Memory Predicates](contracts-memory-predicates.md)
-- [History Variables](contracts-history-variables.md)
-- [Quantifiers](contracts-quantifiers.md)
+- [Requires \& Ensures Clauses](../../contracts/requires-and-ensures/)
+- [Assigns Clause](../../contracts/assigns/)
+- [Memory Predicates](../../contracts/memory-predicates/)
+- [History Variables](../../contracts/history-variables/)
+- [Quantifiers](../../contracts/quantifiers/)

doc/cprover-manual/contracts-history-variables.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # History Variables
 
 ## In Function Contracts

doc/cprover-manual/contracts-invariants.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Invariant Clauses
 
 An _invariant_ clause specifies a property that must be preserved
@@ -141,14 +143,14 @@ A few things to note here:
   using alias analysis of l-values appearing in the loop body.
   However, the analysis is incomplete and may fail to characterize the set for complex loops.
   In such cases, the user must manually annotate the set of modified variables
-  using an [_assigns clause_](contracts-assigns.md).
+  using an [_assigns clause_](../../contracts/assigns/).
 
 - At instrumented code point (6), when we _assume_ `false`,
   observe that this assumption only exists within the `lb <= ub` conditional.
   Therefore, only the symbolic execution path _inside_ this conditional block terminates.
   The code outside of the conditional block continues to be symbolically executed,
   and subsequent assertions do not become vacuously `true`.
 
-[history variables]: contracts-history-variables.md
+[history variables]: ../../contracts/history-variables/
 
 [binary search]: https://en.wikipedia.org/wiki/Binary_search_algorithm

doc/cprover-manual/contracts-loops.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Loop Contracts
 
 CBMC offers support for loop contracts, which includes three basic clauses:
@@ -63,7 +65,7 @@ A developer might be interested in verifying two high-level properties on the lo
 2. the loop must eventually always terminate
 
 To prove the first (memory-safety) property,
-we may declare [_loop invariants_](contracts-invariant.md)
+we may declare [_loop invariants_](../../contracts/invariants/)
 that must be preserved across all loop iterations.
 In this case, two invariant clauses would together imply that `buf[mid]` lookup is always safe.
 The first invariant clause would establish that the bounds (`lb` and `ub`) are always valid:
@@ -80,7 +82,7 @@ __CPROVER_loop_invariant(mid == (lb + ub) / 2L)
 ```
 
 To prove the second (termination) property,
-we may declare a [_decreases clause_](contracts-decreases.md)
+we may declare a [_decreases clause_](../../contracts/decreases/)
 that indicates a bounded numeric measure
 which must monotonically decrease with each loop iteration.
 In this case, it is easy to see that `lb` and `ub` are approaching closer together with each iteration, since either `lb` must increase or `ub` must decrease in each iteration.
@@ -143,10 +145,10 @@ and finally we verify the instrumented GOTO binary with desired checks.
 
 ## Additional Resources
 
-- [Assigns Clause](contracts-assigns.md)
-- [Decreases Clause](contracts-decreases.md)
-- [History Variables](contracts-history-variables.md)
-- [Invariant Clause](contracts-invariant.md)
-- [Quantifiers](contracts-quantifiers.md)
+- [Assigns Clause](../../contracts/assigns/)
+- [Decreases Clause](../../contracts/decreases/)
+- [History Variables](../../contracts/history-variables/)
+- [Invariant Clause](../../contracts/invariants/)
+- [Quantifiers](../../contracts/quantifiers/)
 
 [binary search algorithm]: https://en.wikipedia.org/wiki/Binary_search_algorithm

doc/cprover-manual/contracts-memory-predicates.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Memory Predicates
 
 ### Syntax

doc/cprover-manual/contracts-quantifiers.md

@@ -1,3 +1,5 @@
+[CPROVER Manual TOC](../../)
+
 # Quantifiers
 
 ### Syntax