Merge pull request #4422 from diffblue/manual-fixes2

Minor manual fixes

Author: tautschnig

doc/cprover-manual/api.md

@@ -146,7 +146,7 @@ the array **dest** with the given value.
 
 #### Uninterpreted Functions
 
-Uninterpreted functions are documented \ref man_modelling-nondet "here".
+Uninterpreted functions are documented [here](../modeling/nondeterminism/)).
 
 ### Predefined Types and Symbols
 

doc/cprover-manual/cbmc-assertions.md

@@ -32,11 +32,10 @@ informal description of the assertion. It is shown in the list of
 properties together with the condition.
 
 The assertion language of the CPROVER tools is identical to the language
-used for expressions. Note that \ref man_modelling-nondet
-"nondeterminism"
-can be exploited in order to check a range of choices. As an example,
-the following code fragment asserts that **all** elements of the array
-are zero:
+used for expressions.  Note that
+[nondeterminism](../../modeling-nondeterminism/) can be exploited in order
+to check a range of choices.  As an example, the following code fragment
+asserts that **all** elements of the array are zero:
 
 ```C
 int a[100], i;

doc/cprover-manual/cbmc-tutorial.md

@@ -28,7 +28,7 @@ to detect this problem and reports that the "upper bound property" of
 the buffer has been violated. CBMC is capable of checking these
 lower and upper bounds, even for arrays with dynamic size. A detailed
 discussion of the properties that CBMC can check
-automatically is \ref man_instrumentation-properties "here".
+automatically is [here](../../properties/).
 
 ### First Steps
 
@@ -53,6 +53,7 @@ int puts(const char *s)
 int main(int argc, char **argv)
 {
   puts(argv[2]);
+  return 0;
 }
 ```
 
@@ -74,7 +75,7 @@ preliminary static analysis, which relies on computing a fixed point on
 various [abstract
 domains](http://en.wikipedia.org/wiki/Abstract_interpretation). More
 detail on automatically generated properties is provided
-\ref man_instrumentation-properties "here".
+[here](../../properties/).
 
 Note that these automatically generated properties need not necessarily
 correspond to bugs – these are just *potential* flaws, as abstract
@@ -109,7 +110,7 @@ hold and which do not. Using the SAT solver, CBMC detects that the
 property for the object bounds of `argv` does not hold, and will display:
 
 ```plaintext
-[main.pointer_dereference.6] dereference failure: pointer outside object bounds in argv[(signed long int)2]: FAILURE
+[main.pointer_dereference.6] line 7 dereference failure: pointer outside object bounds in argv[(signed long int)2]: FAILURE
 ```
 
 ### Counterexample Traces
@@ -135,16 +136,18 @@ In the example above, we used a program that starts with a `main`
 function. However, CBMC is aimed at embedded software, and these kinds
 of programs usually have different entry points. Furthermore, CBMC is
 also useful for verifying program modules. Consider the following
-example, called file2.c:
+example, called [file2.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/file2.c):
 
 ```C
 int array[10];
-int sum() {
+
+int sum()
+{
   unsigned i, sum;
 
-  sum=0;
-  for(i=0; i<10; i++)
-    sum+=array[i];
+  sum = 0;
+  for(i = 0; i < 10; i++)
+    sum += array[i];
 
   return sum;
 }
@@ -281,7 +284,7 @@ violates an assertion. Without unwinding assertions, or when using the
 `--depth` command line switch, CBMC does not prove the program correct,
 but it can be helpful to find program bugs. The various command line
 options that CBMC offers for loop unwinding are described in the section
-on \ref man_cbmc-loops "understanding loop unwinding".
+on [understanding loop unwinding](../../cbmc-unwinding/).
 
 ### A Note About Compilers and the ANSI-C Library
 
@@ -319,7 +322,7 @@ be found in the menu *Visual Studio Tools*.
 Note that in both cases, only header files are available. CBMC only
 comes with a small set of definitions, which includes functions such as
 `malloc`. Detailed information about the built-in definitions is
-\ref man_instrumentation-libraries "here".
+[here](../../goto-cc/).
 
 ### Further Reading
 

doc/cprover-manual/file1.c

@@ -5,4 +5,5 @@ int puts(const char *s)
 int main(int argc, char **argv)
 {
   puts(argv[2]);
+  return 0;
 }

doc/cprover-manual/file2.c

@@ -0,0 +1,12 @@
+int array[10];
+
+int sum()
+{
+  unsigned i, sum;
+
+  sum = 0;
+  for(i = 0; i < 10; i++)
+    sum += array[i];
+
+  return sum;
+}

doc/cprover-manual/goto-cc.md

@@ -29,22 +29,25 @@ This example assumes a Unix-like machine.
 1.  Download the sources of wu-ftpd from
     [here](ftp://ftp.wu-ftpd.org/pub/wu-ftpd/wu-ftpd-current.tar.gz).
 
-2.  Unpack the sources by running ` tar xfz wu-ftpd-current.tar.gz`.
+2.  Unpack the sources by running
+
+        tar xfz wu-ftpd-current.tar.gz
 
 3.  Change to the source directory, for example by entering,
-    `cd wu-ftpd-2.6.2`.
+
+        cd wu-ftpd-2.6.2
 
 4.  Configure the project for verification by running:
 
-    `./configure YACC=byacc CC=goto-cc --host=none-none-none`
+        ./configure YACC=byacc CC=goto-cc --host=none-none-none
 
 5.  Build the project by running `make`. This creates multiple model
     files in the `src` directory. Among them is a model for the main
     executable `ftpd`.
 
 6.  Run a model-checker, for example CBMC, on the model file:
 
-        `cbmc src/ftpd`
+        cbmc src/ftpd
 
     CBMC automatically recognizes that the file is a goto binary.
 
@@ -68,7 +71,9 @@ A helpful command that accomplishes this task successfully for many
 projects is:
 
 ```plaintext
-for i in `find . -name Makefile`; do   sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i done
+for i in `find . -name Makefile`; do
+  sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i
+done
 ```
 
 Here are additional examples on how to use goto-cc:

doc/cprover-manual/properties.md

@@ -136,8 +136,8 @@ program, or it is desirable to replace bodies of functions with certain
 predetermined stubs (for example to confirm that these functions are never
 called, or to indicate that these functions will never return). For this purpose
 goto-instrument provides the `--generate-function-body` option, that takes a
-regular expression (in [ECMAScript syntax]
-(http://en.cppreference.com/w/cpp/regex/ecmascript)) that describes the names of
+regular expression (in [ECMAScript
+syntax](http://en.cppreference.com/w/cpp/regex/ecmascript)) that describes the names of
 the functions to generate. Note that this will only generate bodies for
 functions that do not already have one; If one wishes to replace the body of a
 function with an existing definition, the `--remove-function-body` option can be
@@ -193,14 +193,14 @@ Now, we can compile the program and detect that the error functions are indeed
 called by invoking these commands:
 
 ```
-    goto-cc error_example.c -o error_example.goto
-    # Replace all functions ending with _error
-    # (Excluding those starting with __)
-    # With ones that have an assert(false) body
-    goto-instrument error_example.goto error_example_replaced.goto \
-      --generate-function-body '(?!__).*_error' \
-      --generate-function-body-options assert-false
-    cbmc error_example_replaced.goto
+goto-cc error_example.c -o error_example.goto
+# Replace all functions ending with _error
+# (Excluding those starting with __)
+# With ones that have an assert(false) body
+goto-instrument error_example.goto error_example_replaced.goto \
+  --generate-function-body '(?!__).*_error' \
+  --generate-function-body-options assert-false
+cbmc error_example_replaced.goto
 ```
 
 Which gets us the output

doc/cprover-manual/test-suite.md

@@ -1,11 +1,11 @@
-[CPROVER Manual TOC](../../)
+[CPROVER Manual TOC](../)
 
 ## Test Suite Generation with CBMC
 
 ### A Small Tutorial with a Case Study
 
 We assume that CBMC is installed on your system. If not, follow
-\ref man_install-cbmc "these instructions".
+[these instructions](../../installation/).
 
 CBMC can be used to automatically generate test cases that satisfy a
 certain [code coverage](https://en.wikipedia.org/wiki/Code_coverage)
@@ -36,83 +36,83 @@ the figure below.
 ![The pid controller](https://github.com/diffblue/cbmc/raw/develop/doc/assets/pid.png "The pid controller")
 
 ```
-    01: // CONSTANTS:
-    02: #define MAX_CLIMB_SUM_ERR 10
-    03: #define MAX_CLIMB 1
-    04:
-    05: #define CLOCK 16
-    06: #define MAX_PPRZ (CLOCK*600)
-    07:
-    08: #define CLIMB_LEVEL_GAZ 0.31
-    09: #define CLIMB_GAZ_OF_CLIMB 0.75
-    10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
-    11: #define CLIMB_PGAIN -0.03
-    12: #define CLIMB_IGAIN 0.1
-    13:
-    14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
-    15: const float climb_pgain=CLIMB_PGAIN;
-    16: const float climb_igain=CLIMB_IGAIN;
-    17: const float nav_pitch=0;
-    18:
-    19: /** PID function INPUTS */
-    20: // The user input: target speed in vertical direction
-    21: float desired_climb;
-    22: // Vertical speed of the UAV detected by GPS sensor
-    23: float estimator_z_dot;
-    24:
-    25: /** PID function OUTPUTS */
-    26: float desired_gaz;
-    27: float desired_pitch;
-    28:
-    29: /** The state variable: accumulated error in the control */
-    30: float climb_sum_err=0;
-    31:
-    32: /** Computes desired_gaz and desired_pitch */
-    33: void climb_pid_run()
-    34: {
-    35:
-    36:   float err=estimator_z_dot-desired_climb;
-    37:
-    38:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
-    39:
-    40:   float pprz=fgaz*MAX_PPRZ;
-    41:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-    42:
-    43:   /** pitch offset for climb */
-    44:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
-    45:   desired_pitch=nav_pitch+pitch_of_vz;
-    46:
-    47:   climb_sum_err=err+climb_sum_err;
-    48:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
-    49:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
-    50:
-    51: }
-    52:
-    53: int main()
-    54: {
-    55:
-    56:   while(1)
-    57:   {
-    58:     /** Non-deterministic input values */
-    59:     desired_climb=nondet_float();
-    60:     estimator_z_dot=nondet_float();
-    61:
-    62:     /** Range of input values */
-    63:     __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-    64:     __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-    65:
-    66:     __CPROVER_input("desired_climb", desired_climb);
-    67:     __CPROVER_input("estimator_z_dot", estimator_z_dot);
-    68:
-    69:     climb_pid_run();
-    70:
-    71:     __CPROVER_output("desired_gaz", desired_gaz);
-    72:     __CPROVER_output("desired_pitch", desired_pitch);
-    73:
-    74:   }
-    75:
-    76:   return 0;
-    77: }
+01: // CONSTANTS:
+02: #define MAX_CLIMB_SUM_ERR 10
+03: #define MAX_CLIMB 1
+04:
+05: #define CLOCK 16
+06: #define MAX_PPRZ (CLOCK*600)
+07:
+08: #define CLIMB_LEVEL_GAZ 0.31
+09: #define CLIMB_GAZ_OF_CLIMB 0.75
+10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
+11: #define CLIMB_PGAIN -0.03
+12: #define CLIMB_IGAIN 0.1
+13:
+14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
+15: const float climb_pgain=CLIMB_PGAIN;
+16: const float climb_igain=CLIMB_IGAIN;
+17: const float nav_pitch=0;
+18:
+19: /** PID function INPUTS */
+20: // The user input: target speed in vertical direction
+21: float desired_climb;
+22: // Vertical speed of the UAV detected by GPS sensor
+23: float estimator_z_dot;
+24:
+25: /** PID function OUTPUTS */
+26: float desired_gaz;
+27: float desired_pitch;
+28:
+29: /** The state variable: accumulated error in the control */
+30: float climb_sum_err=0;
+31:
+32: /** Computes desired_gaz and desired_pitch */
+33: void climb_pid_run()
+34: {
+35:
+36:   float err=estimator_z_dot-desired_climb;
+37:
+38:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
+39:
+40:   float pprz=fgaz*MAX_PPRZ;
+41:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
+42:
+43:   /** pitch offset for climb */
+44:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
+45:   desired_pitch=nav_pitch+pitch_of_vz;
+46:
+47:   climb_sum_err=err+climb_sum_err;
+48:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
+49:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
+50:
+51: }
+52:
+53: int main()
+54: {
+55:
+56:   while(1)
+57:   {
+58:     /** Non-deterministic input values */
+59:     desired_climb=nondet_float();
+60:     estimator_z_dot=nondet_float();
+61:
+62:     /** Range of input values */
+63:     __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
+64:     __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
+65:
+66:     __CPROVER_input("desired_climb", desired_climb);
+67:     __CPROVER_input("estimator_z_dot", estimator_z_dot);
+68:
+69:     climb_pid_run();
+70:
+71:     __CPROVER_output("desired_gaz", desired_gaz);
+72:     __CPROVER_output("desired_pitch", desired_pitch);
+73:
+74:   }
+75:
+76:   return 0;
+77: }
 ```
 
 To test the PID controller, we construct a main control loop,
@@ -196,7 +196,8 @@ instrumented goals in the PID function `climb_pid_run`, the loop must be
 unwound enough times. For example, `climb_pid_run` needs to
 be called at least six times for evaluating the condition
 `climb_sum_err>MAX_CLIMB_SUM_ERR` in line 48 to *true*. This corresponds
-to Test 5. To learn more about loop unwinding take a look at [Understanding Loop Unwinding](cbmc-loops.shtml).
+to Test 5. To learn more about loop unwinding take a look at [Understanding Loop
+Unwinding](../../cbmc-unwinding/).
 
 In this tutorial, we present the automatic test suite generation
 functionality of CBMC, by applying the MC/DC code coverage criterion to