Merge branch 'fix/andre/a-few-kernel-typos' into 'master'

[Kernel] fix a few typos, reword some comments

See merge request frama-c/frama-c!4343

src/kernel_internals/typing/populate_spec.mli

@@ -20,10 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** This module is used to generate missing specifications Options
+(** This module is used to generate missing specifications. Options
     {!Kernel.GeneratedDefaultSpec}, {!Kernel.GeneratedSpecMode} and
-    {!Kernel.GeneratedSpecCustom} can be used to chose in details which clause
-    to generate in which cases.
+    {!Kernel.GeneratedSpecCustom} can be used to choose precisely which clause
+    to generate in which case.
     @since Frama-C+dev
 *)
 
@@ -58,7 +58,7 @@ type t_requires = identified_predicate list
 type t_terminates = identified_predicate option
 
 (** Type of a function that, given a {!Kernel_function.t} and a
-    {!Cil_types.spec}, returns a clause. Accepted clause types includes
+    {!Cil_types.spec}, returns a clause. Accepted clause types include
     {!t_exits}, {!t_assigns}, {!t_requires}, {!t_allocates} and {!t_terminates}.
 *)
 type 'a gen = (kernel_function -> spec -> 'a)
@@ -69,8 +69,8 @@ type status = Property_status.emitted_status
 (** [register ?gen_exits ?gen_requires ?status_allocates ... name] registers a
     new mode called [name] which can then be used for specification generation
     (see {!Kernel.GeneratedSpecMode} and {!Kernel.GeneratedSpecCustom}). All
-    parameters except [name] are optionals, meaning default action (mode
-    Frama-C) will be performed if left unspecified (triggers a warnings).
+    parameters except [name] are optional, meaning default action (mode
+    Frama-C) will be performed if left unspecified (triggers a warning).
 *)
 val register :
   ?gen_exits:t_exits gen -> ?status_exits:status ->

src/kernel_services/ast_data/annotations.mli

@@ -599,7 +599,7 @@ val global_state: State.t
 (**************************************************************************)
 
 val populate_spec_ref: (kernel_function -> funspec -> bool) ref
-[@@ deprecated "Uses Populate_spec.populate_funspec instead."]
+[@@ deprecated "Use Populate_spec.populate_funspec instead."]
 
 val unsafe_add_global: Emitter.t -> global_annotation -> unit
 val register_funspec:

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1465,9 +1465,10 @@ module GeneratedSpecMode =
       let default = "frama-c"
       let arg_name = "mode"
       let help =
-        "Select which mode will be used to generate missing specifications, \
-         can be either frama-c, acsl, safe or any name of custom registered \
-         modes (defaults to frama-c). See user manual for more informations."
+        "Select which mode will be used to generate missing specifications. \
+         Can be one of: frama-c, acsl, safe, or the name of a custom \
+         registered mode (defaults to frama-c). See user manual for more \
+         information."
     end)
 
 let () = Parameter_customize.set_group normalisation
@@ -1485,8 +1486,8 @@ module GeneratedSpecCustom =
       let arg_name = "c1:m1,c2:m2,..."
       let default = Datatype.String.Map.empty
       let help =
-        "Fine-tune missing specificationss generation by manually choosing \
-         modes for each clause. See user manual for more informations."
+        "Fine-tune missing specification generation by manually choosing \
+         modes for each clause. See user manual for more information."
     end)
 
 let normalization_parameters () =