From 81c3532f986c342ca83d59f43fb6889143850aa7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 11 Feb 2022 11:06:26 +0100
Subject: [PATCH] [Eva] Minor changes in the documentation of Eva.mli.
---
src/plugins/value/Eva.mli | 21 ++++++++++-----------
src/plugins/value/engine/analysis.mli | 7 +++----
src/plugins/value/eval.mli | 4 ++--
src/plugins/value/register.mli | 2 +-
src/plugins/value/utils/eva_annotations.mli | 10 +++++-----
src/plugins/value/value_parameters.mli | 2 ++
6 files changed, 23 insertions(+), 23 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 6c935365f41..2047779dc25 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 06195f65789..4ad30452ccc 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 4c7bcc873aa..0c7808b6607 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 8dd1c29c58b..0f54ee77645 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 69cd10db0d0..5b206536c55 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 41cd18d4647..14c4e47e61a 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
--
GitLab