[eacsl:doc] Update comments

src/plugins/e-acsl/src/code_generator/memory_translate.ml

@@ -55,7 +55,7 @@ let term_to_exp_ref
     Hence [Range_elimination_exception] must be raised. *)
 exception Range_elimination_exception
 
-(* Takes a [toffset] and checks whether it contains an index that is a set *)
+(* Take a [toffset] and check whether it contains an index that is a set *)
 let rec has_set_as_index = function
   | TNoOffset ->
     false
@@ -64,8 +64,8 @@ let rec has_set_as_index = function
   | TModel(_, toffset) | TField(_, toffset) ->
     has_set_as_index toffset
 
-(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
-   Raises [Range_elimination_exception] whether either the operation is unsound
+(* Perform Range Elimination on index [TIndex(term, offset)]. Term part.
+   Raise [Range_elimination_exception] whether either the operation is unsound
    or we don't support the construction yet. *)
 let eliminate_ranges_from_index_of_term ~loc t =
   match t.term_node with
@@ -77,8 +77,8 @@ let eliminate_ranges_from_index_of_term ~loc t =
   | _ ->
     raise Range_elimination_exception
 
-(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
-   Raises [Range_elimination_exception], through [eliminate_ranges_from_
+(* Perform Range Elimination on index [TIndex(term, offset)]. Offset part.
+   Raise [Range_elimination_exception], through [eliminate_ranges_from_
    index_of_term], whether either the operation is unsound or we don't support
    the construction yet. *)
 let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =

src/plugins/e-acsl/src/code_generator/memory_translate.mli

@@ -22,15 +22,15 @@
 
 open Cil_types
 
-(* Create calls to a few memory builtins.
+(* Create calls to a few memory built-ins.
    Partial support for ranges is provided. *)
 
 val call:
   loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
   exp * Env.t
-(* [call ~loc kf name ctx env t] creates a call to the E-ACSL memory builtin
+(* [call ~loc kf name ctx env t] creates a call to the E-ACSL memory built-in
    identified by [name] which only requires a single argument, namely the
-   pointer under study. The supported builtins are:
+   pointer under study. The supported built-ins are:
    [base_addr], [block_length], [offset] and [freeable]. *)
 
 val call_with_size:
@@ -47,7 +47,7 @@ val call_valid:
   loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
   predicate -> exp * Env.t
 (* [call_valid ~loc kf name ctx env t p] creates a call to the E-ACSL memory
-   builtin [valid] or [valid_read] according to [name].
+   built-in [valid] or [valid_read] according to [name].
    [t] can denote ranges of memory locations.
    [p] is the predicate under testing. *)