diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 6c935365f412bd32d06873384effb8fd7ee8d376..2047779dc2581f8be386fe36f48c4bfd4a4bcd3f 100644
--- a/src/plugins/value/Eva.mli
+++ b/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
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 06195f65789282d7eed2cb81a49704690214ba9f..4ad30452ccc3bcdc253dfdc88dd2bcefefaf91af 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/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. *)
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 4c7bcc873aaf1f46ce1d865e07102f84a391805b..0c7808b6607d3199d63b59b321bb4a686797018f 100644
--- a/src/plugins/value/eval.mli
+++ b/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:
diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli
index 8dd1c29c58ba6d614d2485d39ca054f4c78d6bd7..0f54ee776453869a4b44e2675c264a5535429fb9 100644
--- a/src/plugins/value/register.mli
+++ b/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
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 69cd10db0d0dce92acc79c6f5f34c36a124e012c..5b206536c557f1b287c1c7ea9a76d2759642d370 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/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. *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 41cd18d46474d6a4b439f07f8fcc8bf77e2700dd..14c4e47e61ae888414a7e61a743f6f1af796a0dc 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/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