WIP remove manual

Author: hannes-steffenhagen-diffblue

doc/cbmc-user-manual.md

@@ -2014,27 +2014,27 @@ Flag                         |  Check
 `--uninitialized-check`      |  add checks for uninitialized locals (experimental)
 `--error-label label`        |  check that given label is unreachable
 
-#### Generating/Replacing function bodies
+#### Generating function bodies
 
 Sometimes implementations for called functions are not available in the goto
 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` and
-`--replace-function-body` options, that take a regular expression (in
-[ECMAScript syntax](http://en.cppreference.com/w/cpp/regex/ecmascript)) that
-describes the names of the functions to generate or replace, the difference
-being that `--generate-function-body` will only generate bodies of functions
-that do not already have one, whereas `--replace-function-body` will do this and
-in addition also replace existing bodies of functions with the stub.
-
-The shape of the stub itself can be chosen with the `--replace-function-body-options`
-parameter, which can take the following values:
+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
+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
+used to remove the body of the function prior to generating a new one.
+
+The shape of the stub itself can be chosen with the
+`--generate-function-body-options` parameter, which can take the following
+values:
 
  Option                      | Result
 -----------------------------|-------------------------------------------------------------
  `nondet-return`             | Do nothing and return a nondet result (this is the default)
- `empty`                     | Delete the body of the function
  `assert-false`              | Make the body contain an assert(false)
  `assume-false`              | Make the body contain an assume(false)
  `assert-false-assume-false` | Combines assert-false and assume-false
@@ -2081,8 +2081,8 @@ called by invoking these commands
     # (Excluding those starting with __)
     # With ones that have an assert(false) body
     goto-instrument error_example.goto error_example_replaced.goto \
-      --replace-function-body '(?!__).*_error' \
-      --replace-function-body-options assert-false
+      --generate-function-body '(?!__).*_error' \
+      --generate-function-body-options assert-false
     cbmc error_example_replaced.goto
 
 Which gets us the output
@@ -2096,16 +2096,16 @@ Which gets us the output
 > VERIFICATION FAILED
 
 As opposed to the verification success we would have gotten without the
-replacement
+generation.
 
 
 The havoc option takes further parameters `globals` and `params` with this
 syntax: `havoc[,globals:<regex>][,params:<regex>]` (where the square brackets
 indicate an optional part). The regular expressions have the same format as the
-those for the `--replace-function-body` and `--generate-function-body` options
-and indicate which globals and function parameters should be set to nondet. All
-regular expressions require exact matches (i.e. the regular expression `ab?`
-will match 'a' and 'b' but not 'adrian' or 'bertha').
+those for the `--generate-function-body` option and indicate which globals and
+function parameters should be set to nondet. All regular expressions require
+exact matches (i.e. the regular expression `a|b` will match 'a' and 'b' but not
+'adrian' or 'bertha').
 
 Example: With a C program like this
 
@@ -2120,8 +2120,8 @@ Example: With a C program like this
 And the command line
 
     goto-instrument in.goto out.goto
-      --replace-function-body do_something_with_complex
-      --replace-function-body-options
+      --generate-function-body do_something_with_complex
+      --generate-function-body-options
         'havoc,params:.*,globals:AGlobalComplex'
 
 The goto code equivalent of the following will be generated:
@@ -2133,6 +2133,8 @@ The goto code equivalent of the following will be generated:
         complex->real = nondet_double();
         complex->imag = nondet_double();
       }
+      AGlobalComplex.real = nondet_double();
+      AGlobalComplex.imag = nondet_double();
       return nondet_int();
     }
 
@@ -2159,8 +2161,8 @@ Code like this will be generated:
     }
 
 Note that no attempt to follow the `next` pointer is made. If an array of
-unknown (or 0) size is encountered, a diagnostic is emitted and the array
-is not further examined.
+unknown (or 0) size is encountered, a diagnostic is emitted and the array is not
+further examined.
 
 Some care must be taken when choosing the regular expressions for globals and
 functions. Names starting with `__` are reserved for internal purposes; For