From 94e43ad577e7a1362b8b577fcb52a9cfb8906bb7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 26 Jan 2024 12:07:37 +0100
Subject: [PATCH] [doc] update API doc
---
src/kernel_internals/runtime/boot.mli | 7 ++--
.../plugin_entry_points/async.mli | 36 ++++++++++---------
src/kernel_services/visitors/visitor.mli | 2 +-
src/libraries/utils/command.mli | 4 ++-
src/plugins/eva/Eva.mli | 9 +----
src/plugins/eva/utils/results.mli | 9 +----
src/plugins/rte/RteGen.mli | 1 -
src/plugins/slicing/api.mli | 2 +-
src/plugins/slicing/slicingCmds.mli | 2 +-
src/plugins/slicing/slicingInternals.mli | 5 ++-
src/plugins/slicing/slicingState.mli | 7 ++--
src/plugins/slicing/slicingTypes.mli | 5 +--
12 files changed, 37 insertions(+), 52 deletions(-)
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index e5f1df0f519..7655842fb51 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -22,6 +22,7 @@
(** Frama-C main interface.
@since Lithium-20081201
+ @before Frama-C+dev it was in a module named Db
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
module Main : sig
val extend : (unit -> unit) -> unit
@@ -36,12 +37,10 @@ val play_analysis : unit -> unit
*)
val boot : unit -> unit
-(** Start and define the Frama-C kernel main loop. Run by the last linked
- module.
-*)
+(** Start and define the Frama-C kernel main loop. *)
val set_toplevel: ((unit -> unit) -> unit) -> unit
(** Changes the toplevel function to run on boot
@since Frama-C+dev
- @before
+ @before Frama-C+dev it was provided in a different way in Db.Toplevel
*)
diff --git a/src/kernel_services/plugin_entry_points/async.mli b/src/kernel_services/plugin_entry_points/async.mli
index 669045664fb..0775c22c8be 100644
--- a/src/kernel_services/plugin_entry_points/async.mli
+++ b/src/kernel_services/plugin_entry_points/async.mli
@@ -20,17 +20,21 @@
(* *)
(**************************************************************************)
+(** Module dedicated to asynchronous actions.
+ @since Frama-C+dev
+ @before Frama-C+dev these features were in a module named Db
+*)
+
(** Registered daemon on progress. *)
type daemon
-(**
- [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
- daemon to be executed on each {!yield}.
- @param debounced the least amount of time between two successive calls to the
- daemon, in milliseconds (default is 0ms).
- @param on_delayed callback is invoked as soon as the time since the last
- {!yield} is greater than [debounced] milliseconds (or 100ms at least).
- @param on_finished callback is invoked when the callback is unregistered.
+(** [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
+ daemon to be executed on each {!yield}.
+ @param debounced the least amount of time between two successive calls to
+ the daemon, in milliseconds (default is 0ms).
+ @param on_delayed callback is invoked as soon as the time since the last
+ {!yield} is greater than [debounced] milliseconds (or 100ms at least).
+ @param on_finished callback is invoked when the callback is unregistered.
*)
val on_progress :
?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
@@ -48,11 +52,10 @@ val while_progress :
?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
(unit -> bool) -> unit
-(**
- [with_progress ?debounced ?on_delayed trigger job data] executes the given
- [job] on [data] while registering [trigger] as temporary (debounced) daemon.
- The daemon is finally unregistered at the end of the computation.
- Same optional parameters than [on_progress].
+(** [with_progress ?debounced ?on_delayed trigger job data] executes the given
+ [job] on [data] while registering [trigger] as temporary (debounced) daemon.
+ The daemon is finally unregistered at the end of the computation.
+ Same optional parameters than [on_progress].
*)
val with_progress :
?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
@@ -70,10 +73,9 @@ val yield : unit -> unit
will raise a [Cancel] exception. *)
val cancel : unit -> unit
-(**
- Pauses the currently running process for the specified time, in milliseconds.
- Registered daemons, if any, will be regularly triggered during this waiting
- time at a reasonable period with respect to their debouncing constraints.
+(** Pauses the currently running process for the specified time, in milliseconds.
+ Registered daemons, if any, will be regularly triggered during this waiting
+ time at a reasonable period with respect to their debouncing constraints.
*)
val sleep : int -> unit
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 1414b29a14a..c3923794a17 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -24,7 +24,7 @@
open Cil_types
-(** Class type for a Db-aware visitor.
+(** Class type for a database-aware visitor.
This is done by defining auxiliary methods that can be
redefined in inherited classes, while the corresponding ones from
{!Cil.cilVisitor} {b must} retain their values as defined here. Otherwise,
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 6422211b226..b6ce12d959b 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -125,7 +125,9 @@ val command :
When this function returns, the stdout and stderr of the child
process will be filled into the arguments buffer.
@raise Sys_error when a system error occurs
- @raise Async.Cancel when the computation is interrupted or on timeout *)
+ @raise Async.Cancel when the computation is interrupted or on timeout
+ @before Frama-C+dev Async.Cancel was Db.Cancel
+*)
(*
Local Variables:
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 69d7664b7b6..7ee21c551d3 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -181,14 +181,7 @@ end
module Results: sig
(** Eva's result API is a new interface to access the results of an analysis,
- once it is completed. It may slightly change in the future. It aims at
- replacing most uses of [Db.Value], and has some advantages over Db's :
-
- - evaluations uses every available domains and not only Cvalue;
- - the caller may distinguish failure cases when a request is unsucessful;
- - working with callstacks is easy;
- - some common shortcuts are provided (e.g. for extracting ival directly);
- - overall, individual functions are simpler.
+ once it is completed. It may slightly change in the future.
The idea behind this API is that requests must be decomposed in several
steps. For instance, to evaluate an expression :
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index 122dfe95a67..b091f95830f 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -23,14 +23,7 @@
[@@@ api_start]
(** Eva's result API is a new interface to access the results of an analysis,
- once it is completed. It may slightly change in the future. It aims at
- replacing most uses of [Db.Value], and has some advantages over Db's :
-
- - evaluations uses every available domains and not only Cvalue;
- - the caller may distinguish failure cases when a request is unsucessful;
- - working with callstacks is easy;
- - some common shortcuts are provided (e.g. for extracting ival directly);
- - overall, individual functions are simpler.
+ once it is completed. It may slightly change in the future.
The idea behind this API is that requests must be decomposed in several
steps. For instance, to evaluate an expression :
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index dda18706daa..fc927c236f0 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -58,5 +58,4 @@ module Visit : sig
code_annotation * bool
end
-(** Replaces old Db API *)
module Api : module type of Api
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index a09fa2b1cb9..9b36bbdb6b3 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -50,7 +50,7 @@ module Project : sig
@raise SlicingTypes.WrongSlicingLevel if [n] is not valid. *)
val change_slicing_level : Cil_types.kernel_function -> int -> unit
- (** Build a new [Db.Project.t] from all [Slice.t] of a project.
+ (** Build a new [Project.t] from all [Slice.t] of a project.
Can optionally specify how to name the sliced functions
by defining [f_slice_names].
[f_slice_names kf src_visi num_slice] has to return the name
diff --git a/src/plugins/slicing/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index f7c09dd5d8d..1643eef87f1 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -28,7 +28,7 @@ open Pdg_types
is too vast and must be simplified. For example, functions should not
receive variables as names (ie. strings) but directly as zones, possibly
with a hint to the function that does to conversion. Also, most functions
- are slightly modified in Register, then registered in Db. This module and
+ are slightly modified in Register. This module and
Register should be fused. *)
type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index e95e7e115ba..7019d516155 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -21,9 +21,8 @@
(**************************************************************************)
(** {2 Internals types}
- Internals type definitions should be hidden to the outside world,
- but it is not really possible to have abstract types since Slicing has to
- use Db.Slicing functions... *)
+ Internals type definitions should be hidden to the outside world.
+*)
open Cil_datatype
diff --git a/src/plugins/slicing/slicingState.mli b/src/plugins/slicing/slicingState.mli
index 4afe0727826..2e5fbafc5bc 100644
--- a/src/plugins/slicing/slicingState.mli
+++ b/src/plugins/slicing/slicingState.mli
@@ -25,15 +25,16 @@
val get: unit -> SlicingTypes.sl_project
(** Get the state of the slicing project.
- Assume it has already been initialized through {!Db.Slicing.reset_slice}. *)
+ Assume it has already been initialized through {!Slicing.Api.reset_slicing}.
+*)
val may: (unit -> unit) -> unit
(** apply the given closure if the slicing project has been initialized through
- {!Db.Slicing.reset_slice}. *)
+ {!Slicing.Api.reset_slicing}. *)
val may_map: none:'a -> (unit -> 'a) -> 'a
(** apply the given closure if the slicing project has been initialized through
- {!Db.Slicing.reset_slice}, or else return the default value.*)
+ {!Slicing.Api.reset_slicing}, or else return the default value.*)
val self: State.t
(** Internal state of the slicing tool from project viewpoints.
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
index ce42a918acf..c8be622febe 100644
--- a/src/plugins/slicing/slicingTypes.mli
+++ b/src/plugins/slicing/slicingTypes.mli
@@ -39,10 +39,7 @@ exception NoPdg
(** {2 Public types} *)
(** These types are the only one that should be used by the API functions.
- Public type definitions should be hidden to the outside world,
- but it is not really possible to have abstract types since Slicing has to
- use Db.Slicing functions... So, it is up to the user of this module to use
- only this public part.
+ Public type definitions should be hidden to the outside world.
*)
(** contains global things that has been computed so far
--
GitLab