CONTRACTS: documentation fixes

Author: Remi Delmas

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-contract-replacement.md

@@ -35,7 +35,7 @@ ret_t foo(foo_params, write_set_t caller_write_set) {
   __CPROVER_contracts_write_set_ptr_t requires_write_set;
   __CPROVER_contracts_write_set_create(requires_write_set, 0, 0);
 
-  // assume requires clauses
+  // assert requires clauses
   assert(contract::requires(foo_params, requires_write_set));
   assert(contract::requires_contract(foo_params, requires_write_set));
 

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md

@@ -41,7 +41,7 @@ typedef struct __CPROVER_contracts_car_set_t
   __CPROVER_contracts_car_t *elems;
 } __CPROVER_contracts_car_set_t;
 ```
-The allocated size of si set is determined by the maximym number of targets
+The allocated size of a set is determined by the maximum number of targets
 found in the assigns clause of the contract of interest.
 
 Objects for which all bytes are assignable (or freeable) do not need to be

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc.md

@@ -7,7 +7,7 @@ Back to top @ref contracts-dev-spec
 ## Overview
 Frame condition checking consists in checking that a function (and any
 functions it calls) only assigns to memory locations allowed by the contract's
-assigns clause, and only deallocates objects allowed by the contract frees
+assigns clause, and only deallocates objects allowed by the contract's frees
 clause.
 
 To implement frame condition checking we use a method inspired by
@@ -24,7 +24,7 @@ The method consists in:
 In our approach a dynamic frame is represented by the
 @ref __CPROVER_contracts_write_set_t data type defined in @ref cprover_contracts.c.
 
-From an simplified point of view, a @ref __CPROVER_contracts_write_set_t 
+From an simple point of view, a @ref __CPROVER_contracts_write_set_t
 tracks 4 sets of memory locations:
 
 ```c
@@ -51,7 +51,7 @@ struct __CPROVER_contracts_write_set_t {
   of the contract of interest;
 - `allocated` is the set of identifiers of objects
   (as given by `__CPROVER_POINTER_OBJECT(x)`) that were locally allocated
-  since  first entering the function under verification
+  since first entering the function under verification
   (on the stack using `DECL x` or on the heap using
   `x = __CPROVER_allocate(...)`);
 - `deallocated` is the set of pointers `p` that were deallocated using
@@ -64,14 +64,14 @@ allowing to (cf @ref cprover_contracts.c):
 - add contents to `contract_frees`;
 - record an object allocation in `allocated`;
 - record an object deallocation in `deallocated`;
-- check wether a given `car_t` is contained within `contract_assigns` or
-  `allocated`;
-- check wether the object pointed to by a given pointer is contained in
-  `contract_frees` or `allocated`;
+- check wether a given `car_t` describing a location about to be assigned is
+  contained within `contract_assigns` or `allocated`;
+- check wether the object pointed to by a given pointer about to be freed is
+  contained in `contract_frees` or `allocated`;
 - check weither all memory locations of a candidate write set are included in
-- some element of a given reference write set.
+  some element of a given reference write set.
 
-The instrumentation adds as @ref __CPROVER_contracts_write_set_ptr_t parameter
+The instrumentation adds a @ref __CPROVER_contracts_write_set_ptr_t parameter
 to all functions of the GOTO model as follows:
 
 ```c
@@ -81,7 +81,7 @@ ret_t f(<original-parameters>, __CPROVER_contracts_write_set_ptr_t write_set);
 The bodies of the functions are instrumented so that:
 - when the given `write_set` is `NULL`, no checks are performed;
 - when the given `write_set` is not `NULL`, the following checks are performed:
-  - The address range corresponding to the LHS of assignments instructions are
+  - The address ranges corresponding to the LHS of assignments instructions are
     checked for inclusion in `contract_assigns` or `allocated`;
   - stack-allocated objects (`DECL`) and heap-allocated objects
     (`__CPROVER_allocate`) are recorded in `allocated`

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md

@@ -5,7 +5,7 @@ Back to top @ref contracts-dev-spec
 @tableofcontents
 
 The user documentation for function contracts is available at @ref contracts-functions,
-but we briefly remind the structure of a contract below.
+but we briefly remind the developer of the structure of a contract below.
 
 
 A contract is defined by adding one or more clauses to a function declaration or
@@ -34,7 +34,7 @@ __CPROVER_frees(F)
 - A `__CPROVER_requires_contract` clause clause specifies the precondition that
   a function pointer expression P satisfies a contract C, where P may only
   depend on program globals and function parameters;
-- A `__CPROVER_ensures clause (@ref contracts-requires-ensures) specifies a
+- A `__CPROVER_ensures` clause (@ref contracts-requires-ensures) specifies a
   postcondition as boolean expression E that may only depend on program globals,
   function parameters, [memory predicates](@ref contracts-memory-predicates),
   deterministic, side effect-free function calls,
@@ -60,4 +60,4 @@ symbol. We call `contract::foo` the **pure contract** associated with the functi
 ---
  Prev | Next
 :-----|:------
- @ref contracts-dev-spec | @ref contracts-dev-spec-transfo-params
+ @ref contracts-dev-spec | @ref contracts-dev-spec-transform-params

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-spec-rewriting.md

@@ -9,7 +9,7 @@ declaratively by calling special built-ins from regular C functions,
 as described in @ref contracts-assigns and @ref contracts-frees.
 
 Such functions require a rewriting pass in order to turn them into active
-functions that can effectivel populate a write set with new targets.
+functions that can effectively populate a write set with new targets.
 
 ## Rewriting Assigns Clause Functions {#contracts-dev-spec-spec-rewriting-assigns}
 
@@ -20,10 +20,10 @@ signature:
 void foo(parameter-list);
 ```
 
-They can have been generated from an assigns clause or written by the user.
+They can be generated from an assigns clause or written by the user.
 
-To convert them to active functions, the first step is to inline their body to
-remove all function calls to check the result to be loop free.
+To convert them to active functions, the first step is to inline their body and
+remove all function calls, the result of which must be loop-free.
 
 Then, a second pass adds the write set to be filled as new parameter to the
 function:
@@ -95,10 +95,10 @@ signature:
 void foo(parameter-list);
 ```
 
-They can have been generated from an assigns clause or written by the user.
+They can be generated from an assigns clause or written by the user.
 
-To convert them to havoc functions, the first step is to inline their body to
-remove all function calls to check the result to be loop free.
+To convert them to havoc functions, the first step is to inline their body and
+remove all function calls, the result of which must be loop-free.
 
 Then, a second pass adds the write set to be havoced as new parameter to the
 function:

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-transfo-params.md renamed to src/goto-instrument/contracts/doc/developer/contracts-dev-spec-transform-params.md

@@ -1,26 +1,17 @@
-# Program Transformation Overview {#contracts-dev-spec-transfo-params}
+# Program Transformation Overview {#contracts-dev-spec-transform-params}
 
 Back to top @ref contracts-dev-spec
 
 @tableofcontents
 
-The program transformation takes the following parameters:
+These are the main parameter of the program transformation:
 
-```
-goto-instrument --dfcc harness [--enforce-contract f_top/c_top] (--replace-with-contract f/c)* in.gb out.gb
-```
-
-Where:
-- `--dfcc harness` specifies the identifier of the proof harness;
-- `--enforce-contract f_top/c_top` specifies is optional and specifies that
+- `harness_id` specifies the identifier of the proof harness;
+- `(f_top,c_top)` an optional pair and specifies that
   the function `f_top` must be checked against the contract carried by function
-  `c_top`, by the pure contract `contract::c_top`. The contract `/c_top` can be
-  omitted in which case it is assumed that `f_top` needs to be checked against
-  its own contract `contract::f_top`;
-- `--replace-call-with-contract f/c` specifies that function `f` must be replaced
+  `c_top`, by the pure contract `contract::c_top`.
+- `(f,c)` a possibly empty set of pairs where each `f` must be replaced
   with the contract carried by function `c`, i.e. by the pure contract `contract::c`.
-  The contract `/c` can be omitted in which case it is assumed that `f` needs to
-  be replaced by its own contract `contract::f`;
 
 The program transformation steps are applied as follows:
 1. @ref contracts-dev-spec-codegen is applied to all contracts to check or replace;
@@ -29,8 +20,6 @@ The program transformation steps are applied as follows:
 4. @ref contracts-dev-spec-contract-checking is applied to the function to be checked against a contract;
 5. @ref contracts-dev-spec-contract-replacement is applied to each function to be replaced by a contract;
 
-
-
 ---
  Prev | Next
 :-----|:------

src/goto-instrument/contracts/doc/developer/contracts-dev-spec.md

@@ -6,7 +6,7 @@ The program transformation specification is broken down in the following
 sections:
 
 1. @subpage contracts-dev-spec-reminder
-2. @subpage contracts-dev-spec-transfo-params
+2. @subpage contracts-dev-spec-transform-params
 3. @subpage contracts-dev-spec-codegen
 4. @subpage contracts-dev-spec-spec-rewriting
 5. @subpage contracts-dev-spec-dfcc

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

@@ -26,7 +26,7 @@ target            ::= lvalue-expr
 ```
 
 The set of locations writable by a function is the union of the sets of locations
-specified by its assigns clauses, or the empty set of no _assigns_ clause is
+specified by its assigns clauses, or the empty set if no _assigns_ clause is
 specified.
 While, in general, an _assigns_ clause could be interpreted with either
 _writes_ or _modifies_ semantics, this design is based on the former.

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

@@ -18,7 +18,7 @@ Where:
 The program transformation takes the following parameters:
 
 ```
-goto-instrument --dfcc harness [--enforce-contract f] (--replace-with-contract g)* [--apply-loop-contracts] in.gb out.gb
+goto-instrument --dfcc harness [--enforce-contract f] (--replace-call-with-contract g)* [--apply-loop-contracts] in.gb out.gb
 ```
 
 Where: