diff --git a/src/init/boot/boot.ml b/src/init/boot/boot.ml
index d8c8dda3bde9815126f9131d7bdd98ab371d3a04..75a7e2bee4944ff14c332aeb40169f49f9b70e3b 100644
--- a/src/init/boot/boot.ml
+++ b/src/init/boot/boot.ml
@@ -23,57 +23,9 @@
(** Frama-C Entry Point (last linked module).
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-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 () = Db.Main.play := play_analysis
-
-(* ************************************************************************* *)
-(** Booting Frama-C *)
-(* ************************************************************************* *)
-
-(* Main: let's go! *)
-let () =
- Sys.catch_break true;
- let f () =
- ignore (Project.create "default");
- let on_from_name = { Cmdline.on_from_name } in
- Cmdline.parse_and_boot
- ~on_from_name
- ~get_toplevel:(fun () -> !Db.Toplevel.run)
- ~play_analysis
- in
- Cmdline.catch_toplevel_run
- ~f
- ~at_normal_exit:Cmdline.run_normal_exit_hook
- ~on_error:Cmdline.run_error_exit_hook;
-
- (* Implicit exit 0 if we haven't exited yet *)
+let () = Frama_c_kernel.Boot.boot ()
+(* Implicit exit 0 if we haven't exited yet *)
(*
Local Variables:
diff --git a/src/init/boot/dune b/src/init/boot/dune
index ad7b0ab70d1895b2764e5ff15d5cb53d75b5908d..efc35b44550f7dd6480f351b65583393b20b4ca6 100644
--- a/src/init/boot/dune
+++ b/src/init/boot/dune
@@ -24,7 +24,6 @@
(name frama_c_boot)
(public_name frama-c.boot)
(modules boot)
- (flags :standard -open Frama_c_kernel)
(libraries frama_c_kernel)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9f9d354823e420ca49bc6b66786a5b92d37423ab
--- /dev/null
+++ b/src/kernel_internals/runtime/boot.ml
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+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;
+
+ (* Main: let's go! *)
+ Sys.catch_break true;
+ let f () =
+ ignore (Project.create "default");
+ let on_from_name = { Cmdline.on_from_name } in
+ Cmdline.parse_and_boot
+ ~on_from_name
+ ~get_toplevel:(fun () -> !Db.Toplevel.run)
+ ~play_analysis
+ in
+ Cmdline.catch_toplevel_run
+ ~f
+ ~at_normal_exit:Cmdline.run_normal_exit_hook
+ ~on_error:Cmdline.run_error_exit_hook
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e6825efd8a10f4e51b702b8534323601858e0573
--- /dev/null
+++ b/src/kernel_internals/runtime/boot.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+val boot : unit -> unit
+(** Start and define the Frama-C kernel main loop. Run by the last linked
+ module. *)