source: Deliverables/D5.1-5.3/cost-plug-in/plugin/cost.ml @ 1679

Last change on this file since 1679 was 1679, checked in by ayache, 9 years ago

Frama-C plug-in (sources+documentation)

File size: 3.3 KB
Line 
1(**************************************************************************)
2(*                                                                        *)
3(*  This file is part of Frama-C.                                         *)
4(*                                                                        *)
5(*  Copyright (C) 2007-2011                                               *)
6(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
7(*         alternatives)                                                  *)
8(*                                                                        *)
9(*  you can redistribute it and/or modify it under the terms of the GNU   *)
10(*  Lesser General Public License as published by the Free Software       *)
11(*  Foundation, version 2.1.                                              *)
12(*                                                                        *)
13(*  It is distributed in the hope that it will be useful,                 *)
14(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
15(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
16(*  GNU Lesser General Public License for more details.                   *)
17(*                                                                        *)
18(*  See the GNU Lesser General Public License version 2.1                 *)
19(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20(*                                                                        *)
21(**************************************************************************)
22
23(** This is the main module of the plug-in. It makes himself available in
24    Frama-C and apply the cost synthesis on every input file. *)
25
26
27module Self =
28  Plugin.Register
29    (struct
30      let name = "cost synthesis"
31      let shortname = "cost"
32      let module_name = "Cost.Self"
33      let help = "synthesis of the execution cost of each function"
34      let is_dynamic = true
35     end)
36
37
38module Enabled = Self.False
39  (struct
40    let module_name = "Cost.Enabled"
41    let option_name = "-cost"
42    let help = "makes a synthesis of the execution cost of each function"
43    let kind = `Tuning
44   end)
45 
46module Lustre = Self.False
47  (struct
48    let option_name = "-cost-lustre"
49    let help = "input file is a Lustre file"
50    let kind = `Tuning
51   end)
52 
53module Lustre_verify = Self.False
54  (struct
55    let option_name = "-cost-lustre-verify"
56    let help =
57      "input file is a Lustre file, verification of the results requested"
58    let kind = `Tuning
59   end)
60 
61module Lustre_test = Self.False
62  (struct
63    let option_name = "-cost-lustre-test"
64    let help =
65      "input file is a Lustre file, testing of the results requested"
66    let kind = `Tuning
67   end)
68
69
70(** The main function: apply CerCo's compiler and the cost synthesis on each
71    input file. *)
72
73let run () =
74  let lustre_option = Lustre.get () in
75  let lustre_verify_option = Lustre_verify.get () in
76  let lustre_test_option = Lustre_test.get () in
77  if Enabled.get () then
78    let files : Cabs.file list = Ast.UntypedFiles.get () in
79    let files :
80        (Cabs.file * string * string * string * string Misc.String.Map.t) list =
81      List.map
82        (Cerco.apply lustre_option lustre_verify_option lustre_test_option)
83        files in
84    Compute.debug := Self.Debug.get () <> 0 ;
85    List.iter Compute.cost files
86
87let () = Db.Main.extend run
Note: See TracBrowser for help on using the repository browser.