1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
7
(* INRIA (Institut National de Recherche en Informatique et en *)
10
(* you can redistribute it and/or modify it under the terms of the GNU *)
11
(* Lesser General Public License as published by the Free Software *)
12
(* Foundation, version 2.1. *)
14
(* It is distributed in the hope that it will be useful, *)
15
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
16
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
17
(* GNU Lesser General Public License for more details. *)
19
(* See the GNU Lesser General Public License version v2.1 *)
20
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
22
(**************************************************************************)
25
let pdg = Build.compute_pdg kf in
26
(* Annot.add_annotations kf pdg; *)
29
let pretty ?(bw=false) fmt pdg =
30
let kf = PdgTypes.Pdg.get_kf pdg in
31
Format.fprintf fmt "@[[pdg RESULT for %s] :@]@\n@[%a@]"
32
(Kernel_function.get_name kf) (Print.pretty_pdg ~bw) pdg
34
let pretty_node short =
35
if short then PdgTypes.Node.pretty
36
else Print.pretty_node
38
let pretty_key = Print.pretty_key
40
let print_dot pdg filename =
41
Print.build_dot filename pdg;
42
Format.printf "[pdg] dot file generated in %s@." filename
45
Kernel_function.Make_Table
46
(PdgTypes.Pdg.Datatype)
48
let name = "Pdg.State"
49
let dependencies = [] (* postponed *)
54
Options.register_plugin_init
56
let add = Project.Computation.add_dependency Tbl.self in
59
(** Register external functions into Db. *)
61
Db.Pdg.self := Tbl.self;
62
Db.Pdg.get := Tbl.memo compute;
63
Db.Pdg.node_key := PdgTypes.Node.elem_key;
65
Db.Pdg.find_decl_var_node := Sets.find_decl_var_node;
66
Db.Pdg.find_entry_point_node := Sets.find_entry_point_node;
67
Db.Pdg.find_top_input_node := Sets.find_top_input_node;
68
Db.Pdg.find_simple_stmt_nodes := Sets.find_simple_stmt_nodes;
69
Db.Pdg.find_stmt_and_blocks_nodes := Sets.find_stmt_and_blocks_nodes;
70
Db.Pdg.find_stmt_node := Sets.find_stmt_node;
71
Db.Pdg.find_location_nodes_at_stmt := Sets.find_location_nodes_at_stmt;
72
Db.Pdg.find_location_nodes_at_begin := Sets.find_location_nodes_at_begin;
73
Db.Pdg.find_location_nodes_at_end := Sets.find_location_nodes_at_end;
74
Db.Pdg.find_call_ctrl_node := Sets.find_call_ctrl_node;
75
Db.Pdg.find_call_input_node := Sets.find_call_num_input_node;
76
Db.Pdg.find_call_output_node := Sets.find_call_output_node;
77
Db.Pdg.find_input_node := Sets.find_input_node;
78
Db.Pdg.find_ret_output_node := Sets.find_output_node;
79
Db.Pdg.find_output_nodes := Sets.find_output_nodes;
80
Db.Pdg.find_all_inputs_nodes := Sets.find_all_input_nodes;
82
Db.Pdg.find_call_stmts := Sets.find_call_stmts;
84
Db.Pdg.find_code_annot_nodes := Annot.find_code_annot_nodes;
85
Db.Pdg.find_fun_precond_nodes := Annot.find_fun_precond_nodes;
86
Db.Pdg.find_fun_postcond_nodes := Annot.find_fun_postcond_nodes;
88
Db.Pdg.find_call_out_nodes_to_select := Sets.find_call_out_nodes_to_select;
89
Db.Pdg.find_in_nodes_to_select_for_this_call :=
90
Sets.find_in_nodes_to_select_for_this_call;
92
Db.Pdg.direct_dpds := Sets.direct_dpds;
93
Db.Pdg.direct_ctrl_dpds := Sets.direct_ctrl_dpds;
94
Db.Pdg.direct_data_dpds := Sets.direct_data_dpds;
95
Db.Pdg.direct_addr_dpds := Sets.direct_addr_dpds;
97
Db.Pdg.all_dpds := Sets.find_nodes_all_dpds;
98
Db.Pdg.all_ctrl_dpds := Sets.find_nodes_all_ctrl_dpds;
99
Db.Pdg.all_data_dpds := Sets.find_nodes_all_data_dpds;
100
Db.Pdg.all_addr_dpds := Sets.find_nodes_all_addr_dpds;
102
Db.Pdg.direct_uses := Sets.direct_uses;
103
Db.Pdg.direct_ctrl_uses := Sets.direct_ctrl_uses;
104
Db.Pdg.direct_data_uses := Sets.direct_data_uses;
105
Db.Pdg.direct_addr_uses := Sets.direct_addr_uses;
107
Db.Pdg.all_uses := Sets.all_uses;
109
Db.Pdg.custom_related_nodes := Sets.custom_related_nodes;
111
Db.Pdg.iter_nodes := PdgTypes.Pdg.iter_nodes;
113
Db.Pdg.pretty := pretty ;
114
Db.Pdg.pretty_node := pretty_node ;
115
Db.Pdg.pretty_key := pretty_key ;
116
Db.Pdg.extract := print_dot
118
(*Db.Pdg.translate_marks_to_prop := Marks.add_new_marks_to_rqs*)
120
(* polymorphic functions : cannot be registered in Db.
121
* Can be used through Pdg.Register (see Pdg.mli) *)
122
let translate_marks_to_prop = Marks.translate_marks_to_prop
123
let call_out_marks_to_called = Marks.call_out_marks_to_called
124
let in_marks_to_caller = Marks.in_marks_to_caller
125
let translate_in_marks = Marks.translate_in_marks
127
module F_Proj (C : PdgMarks.T_Config) = Marks.F_Proj (C)
131
Cmdline.Pdg.BuildAll.get ()
132
|| not (Cilutil.StringSet.is_empty (Cmdline.Pdg.BuildFct.get ()))
134
if force_pdg then begin
135
Format.fprintf fmt "@\n[pdg] in progress...@.";
137
let fname = Kernel_function.get_name kf in
138
if Cmdline.Pdg.BuildAll.get () ||
139
Cilutil.StringSet.mem fname (Cmdline.Pdg.BuildFct.get ())
141
let pdg = !Db.Pdg.get kf in
142
let bw = Cmdline.Pdg.PrintBw.get () in
143
Format.fprintf fmt "@[%a@]@." (!Db.Pdg.pretty ~bw) pdg;
144
if Cmdline.Pdg.DotBasename.get () <> "" then
146
(Cmdline.Pdg.DotBasename.get ()^"."^fname^".dot")
149
!Db.Semantic_Callgraph.topologically_iter_on_functions do_kf_pdg;
150
if Cmdline.Pdg.BuildAll.get () then
151
Format.fprintf fmt "@\n====== PDG GRAPH COMPUTED ======@.";
154
let () = Db.Main.extend main
156
(** Register options for this computation *)
158
Options.add_plugin ~name:"Program Dependence Graph (experimental)"
162
"-verbose", Arg.Unit Cmdline.Pdg.Verbosity.incr,
163
": increase verbosity level for the pdg plugin (can be repeated).";
166
Arg.Unit Cmdline.Pdg.BuildAll.on,
167
": build the dependence graph of each function for the slicing tool";
170
Arg.String Cmdline.Pdg.BuildFct.add,
171
"f : build the dependence graph for the specified function f";
174
Arg.Unit Cmdline.Pdg.PrintBw.on,
175
": print the co-dependencies rather than the dependencies";
178
Arg.String Cmdline.Pdg.DotBasename.set,
179
"basename : put the PDG of function f in basename.f.dot";
182
Arg.String Cmdline.Pdg.DotPostdomBasename.set,
183
"basename : put the postdominators of function f in basename.f.dot";
189
compile-command: "LC_ALL=C make -C ../.. -j"
added
removed
src/pdg/register.ml
