Source file `boot.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

(** Frama-C Entry Point (last linked module).
    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)

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

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)