Publish documentation

doc/cprover-manual/cbmc-tutorial.md

@@ -176,7 +176,7 @@ the `for` loop in the program. As CBMC performs Bounded Model Checking,
 all loops have to have a finite upper run-time bound in order to
 guarantee that all bugs are found. CBMC can optionally check that enough
 unwinding is performed. As an example, consider the program
-[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch1.c):
+[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch.c):
 
 ```C
 int binsearch(int x)
@@ -333,7 +333,7 @@ comes with a small set of definitions, which includes functions such as
 
 ### Further Reading
 
--   [Understanding Loop Unwinding](../unwinding/)
+-   [Understanding Loop Unwinding](../../cbmc/unwinding/)
 -   [Hardware Verification using ANSI-C Programs as a
     Reference](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html)
 -   [Behavioral Consistency of C and Verilog Programs Using Bounded

doc/cprover-manual/contracts-loops.md

@@ -3,6 +3,7 @@
 # Loop Contracts
 
 CBMC offers support for loop contracts, which includes three basic clauses:
+
 - _invariant_ clause for establishing safety properties
 - _decreases_ clause for establishing termination, and
 - _assigns_ clause for declaring the subset of variables that is modifiable in the loop.

doc/cprover-manual/contracts.md

@@ -15,6 +15,7 @@ Design](https://www.georgefairbanks.com/york-university-contract-based-design-20
 by George Fairbanks.
 
 CBMC currently supports contracts on functions and loops:
+
 - [Function Contracts](../contracts/functions/)
 - [Loop Contracts](../contracts/loops/)
 

doc/cprover-manual/goto-analyzer.md

@@ -18,6 +18,7 @@ iterations or B. possibly false.  In this sense, each tool has its own
 strengths and weaknesses.
 
 To use `goto-analyzer` you need to give options for:
+
 * What [task](#task) to perform after the abstract interpreter has run.
 * How to format the [output](#output).
 * Which [abstract interpreter](#abstractinterpreter) is used.
@@ -48,7 +49,7 @@ goto-analyzer  --verify --three-way-merge --vsd --vsd-values set-of-constants --
 
 I want to discharge obvious conditions and remove unreachable code:
 ```
-goto-analyzer --simplify out.gb --three-way-merge --vsd 
+goto-analyzer --simplify out.gb --three-way-merge --vsd
 ```
 
 
@@ -182,7 +183,7 @@ will likely become the default at some point in the future.
 : This extends `--recursive-interprocedural` by performing a
 "modification aware" merge after function calls.  At the time of
 writing only `--vsd` supports the necessary differential reasoning.
-If you are using `--vsd` this is recommended as it is more accurate 
+If you are using `--vsd` this is recommended as it is more accurate
 with little extra cost.
 
 
@@ -412,7 +413,7 @@ location will use the same domain.  Setting this means that the
 results of other histories will be similar to setting
 `--ahistorical`.  One difference is how and when widening occurs.
 `--one-domain-per-location --loop-unwind n` will wait until `n`
-iterations of a loop have been completed and then will start to widen. 
+iterations of a loop have been completed and then will start to widen.
 
 `--one-domain-per-history`
 : This is the best option to use if you are using a history other than
@@ -430,4 +431,3 @@ instrumentation.  These all function exactly the same as CBMC does.
 It also supports specific analyses which do not fit into the
 configurable scheme above.  At the time of writing this is just
 `--taint` which performs a configurable taint analysis.
-

doc/cprover-manual/index.md

@@ -1,34 +1,34 @@
 # The CPROVER Manual
 
-## 1. [Introduction](introduction/)
+1. [Introduction](introduction/)
 
-## 2. [Installation](installation/)
+2. [Installation](installation/)
 
-## 3. CBMC – Bounded Model Checking
+3. CBMC – Bounded Model Checking
 
-[A Short Tutorial](cbmc/tutorial/),
-[Loop Unwinding](cbmc/unwinding/),
-[Assertion Checking](cbmc/assertions/)
+   * [A Short Tutorial](cbmc/tutorial/)
+   * [Loop Unwinding](cbmc/unwinding/)
+   * [Assertion Checking](cbmc/assertions/)
 
-## 4. [Compositional Reasoning using Code Contracts](contracts/)
+4. [Compositional Reasoning using Code Contracts](contracts/)
 
-## 5. [Goto-Analyzer – Abstract Interpretation](goto-analyzer/)
+5. [Goto-Analyzer – Abstract Interpretation](goto-analyzer/)
 
-## 6. [Test Suite Generation](test-suite/)
+6. [Test Suite Generation](test-suite/)
 
-## 7. [Program Properties](properties/)
+7. [Program Properties](properties/)
 
-## 8. Modeling
+8. Modeling
 
-[Nondeterminism](modeling/nondeterminism/),
-[Assumptions](modeling/assumptions/),
-[Pointers](modeling/pointers/),
-[Floating Point](modeling/floating-point/)
-[Generating Environments](goto-harness/)
+   * [Nondeterminism](modeling/nondeterminism/)
+   * [Assumptions](modeling/assumptions/)
+   * [Pointers](modeling/pointers/)
+   * [Floating Point](modeling/floating-point/)
+   * [Generating Environments](goto-harness/)
 
-## 9. Build Systems
+9. Build Systems
 
-[Integration into Build Systems with goto-cc](goto-cc/),
-[Integration with Visual Studio builds](visual-studio/)
+   * [Integration into Build Systems with goto-cc](goto-cc/)
+   * [Integration with Visual Studio builds](visual-studio/)
 
-## 10. [The CPROVER API Reference](api/)
+10. [The CPROVER API Reference](api/)

doc/cprover-manual/properties.md

@@ -133,14 +133,15 @@ The goto-instrument program supports these checks:
 | `--error-label label`        |  check that given label is unreachable               |
 
 As all of these checks apply across the entire input program, we may wish to
-disable or enable them for selected statements in the program. 
-For example, unsigned overflows can be expected and acceptable in certain 
-instructions even when elsewhere we do not expect them. 
+disable or enable them for selected statements in the program.
+For example, unsigned overflows can be expected and acceptable in certain
+instructions even when elsewhere we do not expect them.
 As of version 5.12, CBMC supports selectively disabling or enabling
 automatically generated properties using pragmas.
 
 
 CPROVER pragmas are handled using a stack:
+
 - `#pragma CPROVER check push` pushes a new level on the pragma stack
 - `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma
   at the top of the stack