package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct