package frama-c

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

Source file register.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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 Pdg_types

let () =
  Cmdline.run_after_extended_stage
    (fun () ->
       State_dependency_graph.add_codependencies
         ~onto:Pdg_tbl.self
         [ From.self ])

let deps =
  [Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]

let () = Pdg_parameters.BuildAll.set_output_dependencies deps

let compute_for_kf kf =
  let all = Pdg_parameters.BuildAll.get () in
  (all && Eva.Results.is_called kf) ||
  Kernel_function.Set.mem kf (Pdg_parameters.BuildFct.get ())

let compute () =
  Eva.Analysis.compute ();
  let do_kf_pdg kf =
    if compute_for_kf kf then
      let pdg = Pdg_tbl.get kf in
      let dot_basename = Pdg_parameters.DotBasename.get () in
      if dot_basename <> "" then
        let fname = Kernel_function.get_name kf in
        Pdg_tbl.print_dot pdg (dot_basename ^ "." ^ fname ^ ".dot")
  in
  Callgraph.Uses.iter_in_rev_order do_kf_pdg;
  let pp_sep fmt () = Format.pp_print_string fmt "," in
  Pdg_parameters.(
    debug "Logging keys : %a"
      (Format.pp_print_list ~pp_sep pp_category) (get_debug_keys ()));
  if Pdg_parameters.BuildAll.get () then
    Pdg_parameters.feedback "====== PDG GRAPH COMPUTED ======"

let compute_once, _ =
  State_builder.apply_once "Pdg.Register.compute_once" deps compute

let output () =
  let bw  = Pdg_parameters.PrintBw.get () in
  let do_kf_pdg kf =
    if compute_for_kf kf then
      let pdg = Pdg_tbl.get kf in
      let header fmt =
        Format.fprintf fmt "PDG for %a" Kernel_function.pretty kf
      in
      Pdg_parameters.printf ~header "@[ @[%a@]@]"
        (PdgTypes.Pdg.pretty_bw ~bw) pdg
  in
  Callgraph.Uses.iter_in_rev_order do_kf_pdg

let something_to_do () =
  Pdg_parameters.BuildAll.get ()
  || not (Kernel_function.Set.is_empty (Pdg_parameters.BuildFct.get ()))

let main () =
  if something_to_do () then
    (compute_once ();
     Pdg_parameters.BuildAll.output output)

let () = Db.Main.extend main


(*
  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