1 (**************************************************************************)
3 (* This file is part of Frama-C. *)
5 (* Copyright (C) 2007-2011 *)
6 (* CEA (Commissariat à l'énergie atomique et aux énergies *)
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. *)
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. *)
18 (* See the GNU Lesser General Public License version 2.1 *)
19 (* for more details (enclosed in the file licenses/LGPLv2.1). *)
21 (**************************************************************************)
23 (** This is the main module of the plug-in. It makes itself available in
24 Frama-C and apply the cost synthesis on every input file. *)
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"
38 module Enabled = Self.False
40 let module_name = "Cost.Enabled"
41 let option_name = "-cost"
42 let help = "makes a synthesis of the execution cost of each function"
46 module Lustre = Self.False
48 let option_name = "-cost-lustre"
49 let help = "input file is a Lustre file"
53 module Lustre_verify = Self.False
55 let option_name = "-cost-lustre-verify"
57 "input file is a Lustre file, verification of the results requested"
61 module Lustre_test = Self.False
63 let option_name = "-cost-lustre-test"
65 "input file is a Lustre file, testing of the results requested"
69 module Old_computation = Self.False
71 let option_name = "-cost-old-computation"
73 "Compute the cost formula by the old way"
77 module Output_suffix = Self.String
79 let option_name = "-cost-output"
81 "Choose the prefix to output the annotation (without -annotated.c)"
87 module Acc_prog = Self.String
89 let option_name = "-cost-acc"
91 "Specify which program must be used for annotation (default: acc)"
97 module Already_instrumented = Self.False
99 let option_name = "-cost-already-instrumented"
100 let help = "input file is already instrumented"
105 (** The main function: apply CerCo's compiler and the cost synthesis on each
109 let save_file fname =
110 Kernel.CodeOutput.set fname ;
114 if Enabled.get () then
115 let lustre_option = Lustre.get () in
116 let lustre_verify_option = Lustre_verify.get () in
117 let lustre_test_option = Lustre_test.get () in
118 let acc_name = Acc_prog.get () in
119 let user_output_filename = Output_suffix.get () in
120 let debug = Self.Debug.get () <> 0 in
121 Compute.debug := debug;
122 Parameters.debug := debug;
123 let files : Cabs.file list = Ast.UntypedFiles.get () in
124 let run_one ((f_name,_) as file) =
125 let (_,new_name,_,_) as file =
126 if Already_instrumented.get () then
127 let default_time = { Cerco.cost_id = "__cost";
128 cost_incr = "__cost_incr";
129 extern_costs = Misc.String.Map.empty;
131 let default_stack_max = Some ({ Cerco.cost_id = "__stack_size_max";
132 cost_incr = "__stack_size_incr";
133 extern_costs = Misc.String.Map.empty;
136 (if user_output_filename <> "" then user_output_filename else
137 (Filename.chop_extension f_name))^"-annotated.c" in
138 (file,new_name,default_time,default_stack_max)
140 let (((fname,_),_,_,_) as file) = Cerco.apply
141 acc_name lustre_option lustre_verify_option lustre_test_option
142 user_output_filename file in
143 Kernel.Files.set [fname] ;
144 File.init_from_cmdline () ;
147 if Old_computation.get ()
148 then Compute.cost file
151 if debug then Printf.printf "Make CFG\n%!" ;
152 Compute_simple.make_CFG () ;
154 if debug then Compute_simple.print_CFG () ;
155 Compute_simple.cost file;
156 Compute_simple_stack_size.cost file;
157 Simplify_terms.add_def_max_logic_info ();
158 if debug then Printf.printf "Save file\n%!" ;
161 List.iter run_one files
163 let () = Db.Main.extend run