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
(**************************************************************************)
24
(** This module can be useful to store some information about differents
25
* elements of a function.
27
* {!module:PdgIndex.Signature} is used to store information
28
* about function inputs/outputs either for the function itself or for its
29
* calls. {!module:PdgIndex.Key} provides keys to identify the different
30
* elements we want to speak about. {!module:PdgIndex.FctIndex} is the main
31
* object that manages the stored information.
33
* This module is used for instance to store the relation between a function
34
* elements and the nodes of its PDG, but it can also be used to store many
37
(** try to add in information while there is already something stored.
38
* Should have used replace function *)
41
(** Some functions doesn't apply to call statement because the stored
42
* information has a different type. *)
43
exception CallStatement
45
(** When we try to find an element that is not in the index *)
48
(** When we compare two things with different locations (no order) *)
51
(** What we call a [Signature] a mapping between keys that represent either a
52
* function input or output, and some information.
56
(** type of a signature where ['a] is the type of the information that we
57
* want to store for each input/output. *)
60
(** key for input elements *)
61
type t_in_key = private
62
InCtrl (** input control point *)
63
| InNum of int (** parameters numbered from 1 *)
64
| InImpl of Locations.Zone.t (** key for implicit inputs.
65
* Used in function signatures only *)
67
type t_out_key = private
68
| OutRet (** key for the output corresponding to the [return] *)
69
| OutLoc of Locations.Zone.t (** key for output locations.
70
used in call signatures only *)
72
(** a key represents either an input or an output of a function. *)
73
type t_key = private In of t_in_key | Out of t_out_key
75
(** build a new, empty signature *)
78
val mk_undef_in_key : Locations.Zone.t -> t_in_key
80
val cmp_in_key : t_in_key -> t_in_key -> int
81
val cmp_out_key : t_out_key -> t_out_key -> int
82
val equal_out_key : t_out_key -> t_out_key -> bool
84
val find_info : 'a t -> t_key -> 'a
85
val find_input : 'a t -> int -> 'a
86
val find_in_ctrl : 'info t -> 'info
87
val find_in_top : 'info t -> 'info
88
val find_in_info : 'info t -> t_in_key -> 'info
89
val find_out_ret : 'a t -> 'a
90
val find_out_info : 'info t -> t_out_key -> 'info
92
val fold : ('a -> t_key * 'b -> 'a) -> 'a -> 'b t -> 'a
93
val fold_num_inputs : ('a -> int * 'b -> 'a) -> 'a -> 'b t -> 'a
94
val fold_impl_inputs :
95
('a -> Locations.Zone.t * 'b -> 'a) -> 'a -> 'b t -> 'a
96
val fold_matching_impl_inputs : Locations.Zone.t ->
97
('a -> Locations.Zone.t * 'b -> 'a) -> 'a -> 'b t -> 'a
98
val fold_all_inputs : ('a -> t_in_key * 'b -> 'a) -> 'a -> 'b t -> 'a
99
val fold_all_outputs : ('a -> t_out_key * 'b -> 'a) -> 'a -> 'b t -> 'a
102
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
103
val pretty_key : Format.formatter -> t_key -> unit
104
val pretty_in_key : Format.formatter -> t_in_key -> unit
107
(** The keys can be used to identify an element of a function.
108
* Have a look at the type [t] to know which kind of elements can be identified.*)
111
(** type to identify a call statement *)
114
(* type annot_key = Cil_types.code_annotation *)
117
SigKey of Signature.t_key
118
(** key for an element of the function signature *)
119
| VarDecl of Cil_types.varinfo
120
(** variable declaration *)
121
| Stmt of Cil_types.stmt
122
(** any statement, except a call *)
123
| CallStmt of t_call_id
124
(** call statement *)
125
| Label of int * Cil_types.label
127
| SigCallKey of t_call_id * Signature.t_key
128
(** key for an element of a call signature *)
129
(* | Annot of annot_key
130
* annotation identified by its kind and id *)
132
val param_key : int -> 'a -> t
133
val implicit_in_key : Locations.Zone.t -> t
138
val out_from_key : Locations.Zone.t -> t
140
val decl_var_key : Cil_types.varinfo -> t
141
val label_key : Cil_types.stmt -> Cil_types.label -> t
142
val stmt_key : Cil_types.stmt -> t
144
val call_key : Cil_types.stmt -> t
145
val call_input_key : Cil_types.stmt -> int -> t
146
val call_output_key : Cil_types.stmt -> Locations.Zone.t -> t
147
val call_outret_key : Cil_types.stmt -> t
148
val call_ctrl_key : Cil_types.stmt -> t
149
val call_topin_key : Cil_types.stmt -> t
151
(* val code_annot_key : Cil_types.code_annotation -> t *)
153
val stmt : t -> Cil_types.stmt option
154
val call_from_id : t_call_id -> Cil_types.stmt
156
val pretty : Format.formatter -> t -> unit
159
(** Mapping between the function elements we are interested in and some
160
* information. Used for instance to associate the nodes with the statements,
161
* or the marks in a slice.
165
(** this type is used to build indexes between program objects and some
166
* information such as the PDG nodes or the slicing marks.
167
*- ['a] if the type of the information to store for each element,
168
*- ['b] if the type of the information
169
that can be attached to call statements
170
* (calls are themselves composed of several elements,
171
* so ['a] information stored for each of them (['a Signature.t]))
175
val create : int -> ('a, 'b) t
176
val length : ('a, 'b) t -> int
178
(** just copy the mapping *)
179
val copy : ('a, 'b) t -> ('a, 'b) t
181
(** merge the two indexes using given functions [merge_a] and [merge_b].
182
* These function are _not_ called when an element is in one index,
183
* but not the other. It is assumed that [merge_x x bot = x]. *)
184
val merge : ('a, 'b) t -> ('a, 'b) t ->
185
('a -> 'a -> 'a) -> ('b -> 'b -> 'b) ->
188
(** get the information stored for the function signature *)
189
val sgn : ('a, 'b) t -> 'a Signature.t
191
(** find the information stored for the key.
192
* Cannot be used for [Key.CallStmt] keys because the type of the stored
193
* information is not the same. See [find_call] instead. *)
194
val find_info : ('a, 'b) t -> Key.t -> 'a
196
(** same than [find_info] except for call statements for which it gives the
197
* list of all the information in the signature of the call. *)
198
val find_all : ('a, 'b) t -> Key.t -> 'a list
200
(** find the information stored for the call and its signature *)
201
val find_call : ('a, 'b) t -> Cil_types.stmt -> 'b option * 'a Signature.t
202
val find_call_key : ('a, 'b) t -> Key.t -> 'b option * 'a Signature.t
204
(** find the information stored for the call *)
205
val find_info_call : ('a, 'b) t -> Cil_types.stmt -> 'b
206
val find_info_call_key : ('a, 'b) t -> Key.t -> 'b
209
(Cil_types.stmt -> 'b option * 'a Signature.t -> 'c -> 'c) ->
210
('a, 'b) t -> 'c -> 'c
212
(** store the information for the key.
213
* @raise AddError if there is already something stored. *)
214
val add : ('a, 'b) t -> Key.t -> 'a -> unit
216
(* val remove : ('a, 'b) t -> Key.t -> unit *)
218
(** store the information for the key. Replace the previously stored
219
* information if any. *)
220
val add_or_replace : ('a, 'b) t -> Key.t -> 'a -> unit
223
('a, 'b) t -> Cil_types.stmt -> 'b -> replace:bool -> unit
224
val add_info_call_key :
225
('a, 'b) t -> Key.t -> 'b -> replace:bool -> unit
added
removed
src/pdg_types/pdgIndex.mli
