← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to src/kernel/boot.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/kernel/boot.ml
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  This file is part of Frama-C.                                         *)
 
4
(*                                                                        *)
 
5
(*  Copyright (C) 2007-2008                                               *)
 
6
(*    CEA (Commissariat � l'�nergie Atomique)                             *)
 
7
(*                                                                        *)
 
8
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
 
9
(*  Lesser General Public License as published by the Free Software       *)
 
10
(*  Foundation, version 2.1.                                              *)
 
11
(*                                                                        *)
 
12
(*  It is distributed in the hope that it will be useful,                 *)
 
13
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
 
14
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
 
15
(*  GNU Lesser General Public License for more details.                   *)
 
16
(*                                                                        *)
 
17
(*  See the GNU Lesser General Public License version 2.1                 *)
 
18
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
 
19
(*                                                                        *)
 
20
(**************************************************************************)
 
21
 
 
22
(* $Id: boot.ml,v 1.33 2008/11/18 12:13:41 uid568 Exp $ *)
 
23
 
 
24
(** Frama-C Entry Point (last linked module).
 
25
    @plugin development guide *)
 
26
 
 
27
(* ************************************************************************* *)
 
28
(** Registering options for debugging project *)
 
29
(* ************************************************************************* *)
 
30
 
 
31
let dump_dependencies () =
 
32
  let _except =
 
33
    Project.Selection.remove Cmdline.Machdep.self
 
34
      (Project.Selection.remove Cmdline.MainFunction.self
 
35
         (Project.Selection.remove Cmdline.LibEntry.self
 
36
            (Cmdline.get_selection ())))
 
37
  in
 
38
  Project.Computation.dump_dependencies (*~except*) 
 
39
    "computation_dependencies.dot"
 
40
 
 
41
let project_debug =
 
42
    [ "-debug", 
 
43
      Arg.Int Project.set_debug_level,      
 
44
      "Level of debug for project";
 
45
      
 
46
      "-dump", Arg.Unit dump_dependencies, "Dump dependencies" ]
 
47
 
 
48
let () = Options.add_cmdline ~name:"project" ~debug:project_debug []
 
49
 
 
50
(* Journal options *)
 
51
let () = 
 
52
  Options.add_cmdline 
 
53
    ~name:"journalization"
 
54
    [ "-journal-disable",
 
55
      Arg.Unit Cmdline.Journal.Disable.on,
 
56
      ": do not output any journal";
 
57
      "-journal-name",
 
58
      Arg.String Cmdline.Journal.Name.set,
 
59
      ": set the filename of the journal (do not write any extension)";
 
60
    ]
 
61
 
 
62
(* ************************************************************************* *)
 
63
(** Adding some internal state dependencies *)
 
64
(* ************************************************************************* *)
 
65
 
 
66
let () =
 
67
  Project.Computation.add_dependency Alarms.self Db.Value.self;
 
68
  Binary_cache.MemoryFootprint.depend Cmdline.MemoryFootprint.self;
 
69
  Buckx.MemoryFootprint.depend Cmdline.MemoryFootprint.self;
 
70
  List.iter 
 
71
    Cil_state.depend 
 
72
    [ Cmdline.SimplifyCfg.self;
 
73
      Cmdline.KeepSwitch.self;
 
74
      Cmdline.UnrollingLevel.self;
 
75
      Cmdline.Constfold.self;
 
76
      Cmdline.ReadAnnot.self;
 
77
      Cmdline.PreprocessAnnot.self ]
 
78
 
 
79
(* ************************************************************************* *)
 
80
(** Booting Frama-C *)
 
81
(* ************************************************************************* *)
 
82
 
 
83
(* Customisation of non-projectified CIL parameters.
 
84
   (projectified CIL parameters must be initialised with {!Cil.initCIL}). *)
 
85
let boot_cil () =
 
86
  Cabs2cil.forceRLArgEval := false;
 
87
  Cil.miscState.Cil.lineDirectiveStyle <- None;
 
88
  (*  Cil.lineDirectiveStyle := Some LinePreprocessorInput;*)
 
89
  Cil.miscState.Cil.printCilAsIs <- Cmdline.Debug.get () > 0;
 
90
  Mergecil.ignore_merge_conflicts := true;
 
91
  Pretty.flushOften := true
 
92
 
 
93
(* Main: let's go! *)
 
94
let () =
 
95
  File.cxx_suffixes := Db.Cxx.suffixes;
 
96
  Kind.version := Version.version;
 
97
  boot_cil ();
 
98
  Sys.catch_break true;
 
99
  !Dynamic.include_all_module ();
 
100
  Journal.start ();
 
101
  at_exit Journal.write;
 
102
  Options.parse_cmdline ();
 
103
  if Cmdline.Journal.Disable.get () then begin
 
104
    Journal.clear ~restart:false ();
 
105
    Journal.stop ()
 
106
  end;
 
107
  if Cmdline.Journal.Name.is_set () then 
 
108
    Journal.set_name (Cmdline.Journal.Name.get ());
 
109
  Options.initialize_toplevels ()
 
110
 
 
111
(*
 
112
Local Variables:
 
113
compile-command: "LC_ALL=C make -C ../.. -j"
 
114
End:
 
115
*)