package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file api.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

(* ---------------------------------------------------------------------- *)
(** Global data management *)

let split_slice s =
  SlicingParameters.debug ~level:1 "[Api.split_slice]";
  SlicingProject.split_slice s

let merge_slices ff_1 ff_2 ~replace =
  SlicingParameters.debug ~level:1 "[Api.merge_slices]";
  SlicingProject.merge_slices ff_1 ff_2 replace

let copy_slice ff =
  SlicingParameters.debug ~level:1 "[Api.copy_slice]";
  Fct_slice.copy_slice ff

(* ---------------------------------------------------------------------- *)
(** {1 Global setting } *)

let self = SlicingState.self

(* ---------------------------------------------------------------------- *)

let set_modes calls callers sliceUndef keepAnnotations () =
  SlicingParameters.Mode.Calls.set calls ;
  SlicingParameters.Mode.Callers.set callers ;
  SlicingParameters.Mode.SliceUndef.set sliceUndef;
  SlicingParameters.Mode.KeepAnnotations.set keepAnnotations

let set_modes ?(calls=SlicingParameters.Mode.Calls.get ())
    ?(callers=SlicingParameters.Mode.Callers.get ())
    ?(sliceUndef=SlicingParameters.Mode.SliceUndef.get ())
    ?(keepAnnotations=SlicingParameters.Mode.KeepAnnotations.get ())
    () =
  set_modes calls callers sliceUndef keepAnnotations ()

(* ---------------------------------------------------------------------- *)

(** {1 Slicing project } *)
module Project = struct

  (** {2 Values } *)

  let default_slice_names = SlicingTransform.default_slice_names

  let reset_slicing = SlicingState.reset_slicing

  let extract ?(f_slice_names=default_slice_names) new_proj_name =
    SlicingTransform.extract ~f_slice_names new_proj_name

  let print_dot ~filename ~title =
    PrintSlice.build_dot_project filename title

  let change_slicing_level = SlicingMacros.change_slicing_level

  (** {2 No needs of Journalization} *)

  let is_directly_called_internal = SlicingMacros.is_src_fun_called
  let is_called = Fct_slice.is_src_fun_called
  let has_persistent_selection = SlicingMacros.has_persistent_selection

  (** {2 Debug} *)

  let pretty = SlicingProject.print_project_and_worklist

end

(* ---------------------------------------------------------------------- *)

(** {1 Mark} *)
module Mark = struct

  type t = SlicingTypes.sl_mark
  let dyn_t = SlicingTypes.dyn_sl_mark

  (** {2 No needs of Journalization} *)

  let compare = SlicingMarks.compare_marks
  let pretty = SlicingMarks.pretty_mark
  let make = SlicingMarks.mk_user_mark
  let is_bottom = SlicingMarks.is_bottom_mark
  let is_spare = SlicingMarks.is_spare_mark
  let is_ctrl = SlicingMarks.is_ctrl_mark
  let is_data = SlicingMarks.is_addr_mark
  let is_addr = SlicingMarks.is_data_mark
  let get_from_src_func = Fct_slice.get_mark_from_src_fun
end

(* ---------------------------------------------------------------------- *)

(** {1 Selection} *)
module Select = struct

  type t = SlicingTypes.sl_select
  let dyn_t = SlicingTypes.Sl_select.ty

  module S = Cil_datatype.Varinfo.Map.Make(SlicingTypes.Fct_user_crit)
  let dyn_set = S.ty
  let empty_selects = Cil_datatype.Varinfo.Map.empty

  include SlicingCmds
  let get_function = get_select_kf

  let merge_internal = SlicingSelect.merge_db_select
  let add_to_selects_internal = SlicingSelect.Selections.add_to_selects
  let iter_selects_internal = SlicingSelect.Selections.iter_selects_internal
  let fold_selects_internal = SlicingSelect.Selections.fold_selects_internal
  let select_stmt_internal = SlicingSelect.select_stmt_computation
  let select_label_internal = SlicingSelect.select_label
  let select_min_call_internal = SlicingSelect.select_minimal_call
  let select_stmt_zone_internal = SlicingSelect.select_stmt_zone
  let select_zone_at_entry_point_internal = SlicingSelect.select_zone_at_entry
  let select_zone_at_end_internal = SlicingSelect.select_zone_at_end
  let select_modified_output_zone_internal = SlicingSelect.select_modified_output_zone
  let select_stmt_ctrl_internal = SlicingSelect.select_stmt_ctrl
  let select_entry_point_internal = SlicingSelect.select_entry_point
  let select_return_internal = SlicingSelect.select_return
  let select_decl_var_internal = SlicingSelect.select_decl_var
  let select_pdg_nodes_internal = SlicingSelect.select_pdg_nodes

  (** {2 Debug} *)

  let pretty = SlicingSelect.print_select

end

(* ---------------------------------------------------------------------- *)

(** {1 Slice} *)
module Slice = struct

  type t = SlicingTypes.sl_fct_slice
  let dyn_t = SlicingTypes.dyn_sl_fct_slice

  let create =
    SlicingProject.create_slice

  let remove =
    SlicingProject.remove_ff

  let remove_uncalled =
    SlicingProject.remove_uncalled_slices

  (** {2 No needs of Journalization} *)

  let get_all = SlicingProject.get_slices
  let get_function = SlicingMacros.get_ff_kf
  let get_callers = SlicingProject.get_slice_callers

  let get_called_slice ff stmt =
    match stmt.skind with
    | Instr (Call _ | Local_init (_, ConsInit _, _)) ->
      fst (Fct_slice.get_called_slice ff stmt)
    | _ -> None

  let get_called_funcs ff stmt =
    match stmt.skind with
    | Instr (Call _) ->
      if snd (Fct_slice.get_called_slice ff stmt) then
        Eva.Results.callee stmt
      else
        []
    | Instr (Local_init (_, ConsInit (f, _, _), _)) -> [ Globals.Functions.get f ]
    | _ -> []

  let get_mark_from_stmt = Fct_slice.get_stmt_mark
  let get_mark_from_label = Fct_slice.get_label_mark
  let get_mark_from_local_var = Fct_slice.get_local_var_mark

  let get_mark_from_formal ff var =
    let kf = SlicingMacros.get_ff_kf ff in
    let param_list = Kernel_function.get_formals kf in
    let rec find n var_list = match var_list with
      | [] -> raise Not_found
      | v :: var_list -> if Cil_datatype.Varinfo.equal v var then n
        else find (n+1) var_list
    in let n = find 1 param_list in
    Fct_slice.get_param_mark ff n

  let get_user_mark_from_inputs = Fct_slice.merge_inputs_m1_mark

  let get_num_id = SlicingMacros.get_ff_id

  let from_num_id kf num =
    List.find
      (fun f -> num = SlicingMacros.get_ff_id f)
      (SlicingProject.get_slices kf)

  (** {2 Debug} *)

  let pretty = SlicingProject.pretty_slice

end

(* ---------------------------------------------------------------------- *)

(** {1 Slicing request} *)
module Request = struct

  let apply_all propagate_to_callers =
    SlicingCmds.apply_all ~propagate_to_callers
  let apply_all ~propagate_to_callers =
    apply_all propagate_to_callers

  let apply_all_internal =
    SlicingCmds.apply_all_actions

  let apply_next_internal =
    SlicingCmds.apply_next_action

  let propagate_user_marks =
    SlicingCmds.topologic_propagation

  let copy_slice = copy_slice

  let split_slice = split_slice

  let merge_slices ff_1 ff_2 ~replace =
    merge_slices ff_1 ff_2 ~replace

  let add_call_slice caller to_call =
    SlicingSelect.call_ff_in_caller ~caller ~to_call
  let add_call_slice ~caller ~to_call =
    add_call_slice caller to_call

  let add_call_fun caller to_call =
    SlicingSelect.call_fsrc_in_caller ~caller ~to_call
  let add_call_fun ~caller ~to_call =
    add_call_fun caller to_call

  let add_call_min_fun caller to_call =
    SlicingSelect.call_min_f_in_caller ~caller ~to_call
  let add_call_min_fun ~caller ~to_call =
    add_call_min_fun caller to_call

  let add_selection =
    SlicingCmds.add_selection

  let add_persistent_selection =
    SlicingCmds.add_persistent_selection

  let add_persistent_cmdline =
    SlicingCmds.add_persistent_cmdline

  (** {2 No needs of Journalization} *)

  let is_request_empty_internal = SlicingProject.is_request_empty

  let add_slice_selection_internal = SlicingSelect.add_ff_selection
  let add_selection_internal = SlicingSelect.add_fi_selection

  (** {2 Debug} *)

  let pretty = SlicingProject.print_proj_worklist

end
(* ---------------------------------------------------------------------- *)
(*
Local Variables:
compile-command: "make -C ../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct