[Eva] Minor changes in the documentation of Eva.mli.

src/plugins/value/Eva.mli

@@ -2,9 +2,8 @@
 
 module Analysis: sig
   val compute : unit -> unit
-  (** Compute the value analysis, if not already computed, using the entry
-      point of the current project. You may set it with
-      {!Globals.set_entry_point}.
+  (** Computes the Eva analysis, if not already computed, using the entry point
+      of the current project. You may set it with {!Globals.set_entry_point}.
       @raise Globals.No_such_entry_point if the entry point is incorrect
       @raise Db.Value.Incorrect_number_of_arguments if some arguments are
       specified for the entry point using {!Db.Value.fun_set_args}, and
@@ -12,7 +11,7 @@ module Analysis: sig
       @plugin development guide *)
 
   val is_computed : unit -> bool
-  (** Return [true] iff the value analysis has been done. *)
+  (** Return [true] iff the Eva analysis has been done. *)
 
   val self : State.t
   (** Internal state of Eva analysis from projects viewpoint. *)
@@ -254,6 +253,8 @@ module Value_results: sig
 end
 
 module Value_parameters: sig
+  (** Configuration of the analysis. *)
+
   (** Returns the list (name, descr) of currently enabled abstract domains. *)
   val enabled_domains: unit -> (string * string) list
 
@@ -286,17 +287,15 @@ module Unit_tests: sig
 end
 
 module Eva_annotations: sig
-  (** Register special annotations to locally guide the partitioning of states
-      performed by an Eva analysis:
+  (** Register special annotations to locally guide the Eva analysis:
 
       - slevel annotations: "slevel default", "slevel merge" and "slevel i"
       - loop unroll annotations: "loop unroll term"
       - value partitioning annotations: "split term" and "merge term"
       - subdivision annotations: "subdivide i"
+  *)
 
-      Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
-
-  (** Annotations tweaking the behavior of the -eva-slevel paramter. *)
+  (** Annotations tweaking the behavior of the -eva-slevel parameter. *)
   type slevel_annotation =
     | SlevelMerge        (** Join all states separated by slevel. *)
     | SlevelDefault      (** Use the limit defined by -eva-slevel. *)
@@ -342,12 +341,12 @@ end
 module Eval: sig
   (** Can the results of a function call be cached with memexec? *)
   type cacheable =
-    | Cacheable      (** Functions whose result can be safely cached *)
+    | Cacheable      (** Functions whose result can be safely cached. *)
     | NoCache        (** Functions whose result should not be cached, but for
                          which the caller can still be cached. Typically,
                          functions printing something during the analysis. *)
     | NoCacheCallers (** Functions for which neither the call, neither the
-                         callers, can be cached *)
+                         callers, can be cached. *)
 end
 
 module Builtins: sig

src/plugins/value/engine/analysis.mli

@@ -88,9 +88,8 @@ val force_compute : unit -> unit
 
 [@@@ api_start]
 val compute : unit -> unit
-(** Compute the value analysis, if not already computed, using the entry
-    point of the current project. You may set it with
-    {!Globals.set_entry_point}.
+(** Computes the Eva analysis, if not already computed, using the entry point
+    of the current project. You may set it with {!Globals.set_entry_point}.
     @raise Globals.No_such_entry_point if the entry point is incorrect
     @raise Db.Value.Incorrect_number_of_arguments if some arguments are
     specified for the entry point using {!Db.Value.fun_set_args}, and
@@ -98,7 +97,7 @@ val compute : unit -> unit
     @plugin development guide *)
 
 val is_computed : unit -> bool
-(** Return [true] iff the value analysis has been done. *)
+(** Return [true] iff the Eva analysis has been done. *)
 
 val self : State.t
 (** Internal state of Eva analysis from projects viewpoint. *)

src/plugins/value/eval.mli

@@ -273,12 +273,12 @@ type recursion = {
 [@@@ api_start]
 (** Can the results of a function call be cached with memexec? *)
 type cacheable =
-  | Cacheable      (** Functions whose result can be safely cached *)
+  | Cacheable      (** Functions whose result can be safely cached. *)
   | NoCache        (** Functions whose result should not be cached, but for
                        which the caller can still be cached. Typically,
                        functions printing something during the analysis. *)
   | NoCacheCallers (** Functions for which neither the call, neither the
-                       callers, can be cached *)
+                       callers, can be cached. *)
 [@@@ api_end]
 (*
 Local Variables:

src/plugins/value/register.mli

@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Functions of the Value plugin registered in {!Db}. Only two functions
+(** Functions of the Value plugin registered in {!Db}. Only three functions
     are exported. *)
 
 val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t

src/plugins/value/utils/eva_annotations.mli

@@ -20,18 +20,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* Note: widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+
 [@@@ api_start]
-(** Register special annotations to locally guide the partitioning of states
-    performed by an Eva analysis:
+(** Register special annotations to locally guide the Eva analysis:
 
     - slevel annotations: "slevel default", "slevel merge" and "slevel i"
     - loop unroll annotations: "loop unroll term"
     - value partitioning annotations: "split term" and "merge term"
     - subdivision annotations: "subdivide i"
+*)
 
-    Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
-
-(** Annotations tweaking the behavior of the -eva-slevel paramter. *)
+(** Annotations tweaking the behavior of the -eva-slevel parameter. *)
 type slevel_annotation =
   | SlevelMerge        (** Join all states separated by slevel. *)
   | SlevelDefault      (** Use the limit defined by -eva-slevel. *)

src/plugins/value/value_parameters.mli

@@ -231,6 +231,8 @@ val register_builtin: string -> unit
 val register_domain: name:string -> descr:string -> unit
 
 [@@@ api_start]
+(** Configuration of the analysis. *)
+
 (** Returns the list (name, descr) of currently enabled abstract domains. *)
 val enabled_domains: unit -> (string * string) list