From de3304d852349bfc1cf735647242a49b39e83cf2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 25 Jan 2024 11:35:28 +0100
Subject: [PATCH] [kernel] moves some (non casual) Db features to Boot
---
src/kernel_internals/runtime/boot.ml | 63 ++++++++++---------
src/kernel_internals/runtime/boot.mli | 15 ++++-
src/kernel_services/plugin_entry_points/db.ml | 9 ---
.../plugin_entry_points/db.mli | 14 -----
src/plugins/aorai/tests/Aorai_test.ml | 5 +-
src/plugins/gui/analyses_manager.ml | 2 +-
src/plugins/gui/design.ml | 2 +-
src/plugins/gui/file_manager.ml | 2 +-
src/plugins/gui/launcher.ml | 2 +-
9 files changed, 52 insertions(+), 62 deletions(-)
diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
index 9f9d354823e..3b40425c8b0 100644
--- a/src/kernel_internals/runtime/boot.ml
+++ b/src/kernel_internals/runtime/boot.ml
@@ -20,37 +20,38 @@
(* *)
(**************************************************************************)
-let boot () =
- let play_analysis () =
- if Kernel.TypeCheck.get () then begin
- if Kernel.Files.get () <> [] || Kernel.TypeCheck.is_set () then begin
- Ast.compute ();
- (* Printing files before anything else (in debug mode only) *)
- if Kernel.debug_atleast 1 && Kernel.is_debug_key_enabled Kernel.dkey_ast
- then File.pretty_ast ()
- end
- end;
- try
- Db.Main.apply ();
- Log.treat_deferred_error ();
- (* Printing code, if required, have to be done at end. *)
- if Kernel.PrintCode.get () then File.pretty_ast ();
- (* Easier to handle option -set-project-as-default at the last moment:
- no need to worry about nested [Project.on] *)
- Project.set_keep_current (Kernel.Set_project_as_default.get ());
- (* unset Kernel.Set_project_as_default, but only if it set.
- This avoids disturbing the "set by user" flag. *)
- if Kernel.Set_project_as_default.get () then
- Kernel.Set_project_as_default.off ()
- with Globals.No_such_entry_point msg ->
- Kernel.abort "%s" msg
- in
- let on_from_name name f =
- try Project.on (Project.from_unique_name name) f ()
- with Project.Unknown_project -> Kernel.abort "no project `%s'." name
- in
- Db.Main.play := play_analysis;
+let toplevel = ref (fun f -> f ())
+let set_toplevel run = toplevel := run
+let play_analysis () =
+ if Kernel.TypeCheck.get () then begin
+ if Kernel.Files.get () <> [] || Kernel.TypeCheck.is_set () then begin
+ Ast.compute ();
+ (* Printing files before anything else (in debug mode only) *)
+ if Kernel.debug_atleast 1 && Kernel.is_debug_key_enabled Kernel.dkey_ast
+ then File.pretty_ast ()
+ end
+ end;
+ try
+ Db.Main.apply ();
+ Log.treat_deferred_error ();
+ (* Printing code, if required, have to be done at end. *)
+ if Kernel.PrintCode.get () then File.pretty_ast ();
+ (* Easier to handle option -set-project-as-default at the last moment:
+ no need to worry about nested [Project.on] *)
+ Project.set_keep_current (Kernel.Set_project_as_default.get ());
+ (* unset Kernel.Set_project_as_default, but only if it set.
+ This avoids disturbing the "set by user" flag. *)
+ if Kernel.Set_project_as_default.get () then
+ Kernel.Set_project_as_default.off ()
+ with Globals.No_such_entry_point msg ->
+ Kernel.abort "%s" msg
+
+let on_from_name name f =
+ try Project.on (Project.from_unique_name name) f ()
+ with Project.Unknown_project -> Kernel.abort "no project `%s'." name
+
+let boot () =
(* Main: let's go! *)
Sys.catch_break true;
let f () =
@@ -58,7 +59,7 @@ let boot () =
let on_from_name = { Cmdline.on_from_name } in
Cmdline.parse_and_boot
~on_from_name
- ~get_toplevel:(fun () -> !Db.Toplevel.run)
+ ~get_toplevel:(fun () -> !toplevel)
~play_analysis
in
Cmdline.catch_toplevel_run
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index e6825efd8a1..23fdd74a8e1 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -20,6 +20,19 @@
(* *)
(**************************************************************************)
+val play_analysis : unit -> unit
+(** Run all the Frama-C analyses. This function should be called only by
+ toplevels.
+ @since Frama-C+dev
+*)
+
val boot : unit -> unit
(** Start and define the Frama-C kernel main loop. Run by the last linked
- module. *)
+ module.
+*)
+
+val set_toplevel: ((unit -> unit) -> unit) -> unit
+(** Changes the toplevel function to run on boot
+ @since Frama-C+dev
+ @before
+*)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 365cbf36d5e..017f5d7e289 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -20,17 +20,8 @@
(* *)
(**************************************************************************)
-open Extlib
-
module Main = struct
include Hook.Make()
- let play = mk_fun "Main.play"
-end
-
-module Toplevel = struct
-
- let run = ref (fun f -> f ())
-
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e7d04befcc2..08f85896583 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -54,11 +54,6 @@ module Main: sig
(** Register a function to be called by the Frama-C main entry point.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
- val play: (unit -> unit) ref
- (** Run all the Frama-C analyses. This function should be called only by
- toplevels.
- @since Beryllium-20090901 *)
-
(**/**)
val apply: unit -> unit
(** Not for casual user. *)
@@ -66,15 +61,6 @@ module Main: sig
end
-module Toplevel: sig
-
- val run: ((unit -> unit) -> unit) ref
- (** Run a Frama-C toplevel playing the game given in argument (in
- particular, applying the argument runs the analyses).
- @since Beryllium-20090901 *)
-
-end
-
(** {3 GUI} *)
(** Registered daemon on progress. *)
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 5cd54943e86..47e9071fd8a 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -50,7 +50,6 @@ let is_suffix suf str =
let extend () =
let myrun =
- let run = !Db.Toplevel.run in
fun f ->
let my_project = Project.create "Reparsing" in
let wp_compute_kf kf =
@@ -71,7 +70,7 @@ let extend () =
then
wp_compute_kf kf
in
- run f;
+ f ();
let tmpdir = Filename.get_temp_dir_name () in
let tmpdir =
match Filename.chop_suffix_opt ~suffix:"/" tmpdir with
@@ -133,6 +132,6 @@ let extend () =
end;
ok:=true (* no error, we can erase the file *)
in
- Db.Toplevel.run := myrun
+ Boot.set_toplevel myrun
let () = extend ()
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index 2c315fb4090..df4382b5254 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -43,7 +43,7 @@ let run title filter_name extension loader
| `EXECUTE ->
let run f =
loader f;
- !Db.Main.play ();
+ Boot.play_analysis ();
host_window#reset ()
in
Option.iter run dialog#filename;
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 2442eb86f71..588d8f05465 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1937,7 +1937,7 @@ let toplevel play =
ignore (Glib.Idle.add (fun () -> in_idle (); false));
GMain.Main.main ()
-let () = Db.Toplevel.run := toplevel
+let () = Boot.set_toplevel toplevel
(*
Local Variables:
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 655eaff92af..3feaf60108f 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -49,7 +49,7 @@ let reparse (host_window: Design.main_window_extension_points) =
Kernel.Files.set [];
Kernel.Files.set files;
Ast.compute ();
- !Db.Main.play ();
+ Boot.play_analysis ();
Source_manager.clear host_window#original_source_viewer)
in
begin match old_helt, succeeded with
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index e6d9dbf1fb4..00b716d11b7 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -35,7 +35,7 @@ let run (host:basic_main) dialog () =
(fun () ->
dialog#destroy ();
Kernel_hook.apply ();
- !Db.Main.play ()));
+ Boot.play_analysis ()));
(* Even if the above operation failed, we try to reset the gui, as the
plugins might have done something before crashing *)
ignore (host#protect ~cancelable:false ~parent:(dialog :> GWindow.window_skel)
--
GitLab