Merge branch 'feature/kernel/move-boot-inside' into 'master'

[Kernel] Move the booting code inside

See merge request frama-c/frama-c!4374

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:

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))

src/kernel_internals/runtime/boot.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/kernel_internals/runtime/boot.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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. *)