diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index e5f1df0f5192cf827e8e70d41c88d63317c7366a..7655842fb51e08f109189576b6d52596385ff1fe 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 669045664fb88adcdb1152f6dee64ef0680a3d39..0775c22c8be984380185674ded31a12a209058e3 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 1414b29a14ab2e24a733bf8be800c2b02743b27f..c3923794a177dbd5ad1d06f446cd814d9d5ff322 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 6422211b226689832f43093ba822de600a2d9175..b6ce12d959bd1b1fe13f54b8e77d182244c525b0 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 69d7664b7b6ef74637f9965bf5978458291749d8..7ee21c551d305b60cadca7ec6460b7d37f67b24b 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 122dfe95a676937703d5ddf4261f7a88147923c1..b091f95830f1e2c6846970a94b84bbafc81e4072 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 dda18706daadcf48439956f31931d0ebd1b5a155..fc927c236f044cafed5879173e5e52dbbaf36457 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 a09fa2b1cb965fd4d3136613d88a645fbe9b5564..9b36bbdb6b32e38f47fdaa55de167f0f70b37f02 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 f7c09dd5d8d44cfae8d7f01aac1033d0b3ca71ec..1643eef87f1a9137962404ddaafb208ce1250e48 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 e95e7e115ba72039b783b304846da7539d898740..7019d516155668f1c031fb98eb18bcab5f8dd5fb 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 4afe0727826260baa2ffbfdc48340a5430a55e96..2e5fbafc5bc5c1e89d56b3aafc8e378765905ac9 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 ce42a918acf0f228645dd4b8ecca2ecaea755bf3..c8be622febe9d45e68dee7b40ad84117768d2a81 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