package frama-c

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

Source file users_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
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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

include
  Plugin.Register
    (struct
      let name = "users"
      let shortname = "users"
      let help = "function callees"
    end)

module ForceUsers =
  False
    (struct
      let option_name = "-users"
      let help = "compute function callees"
    end)

module Users =
  Kernel_function.Make_Table
    (Kernel_function.Hptset)
    (struct
      let name = "Users"
      let size = 17
      let dependencies = [ Eva.Analysis.self; ForceUsers.self ]
    end)

let compute_users _ =
  let process kf =
    if Eva.Results.is_called kf
    then
      let callstacks = Eva.Results.(at_start_of kf |> callstacks) in
      let process_callstack callstack =
        let users = List.tl (List.rev (Eva.Callstack.to_kf_list callstack)) in
        let process_element user =
          ignore
            (Users.memo
               ~change:(Kernel_function.Hptset.add kf)
               (fun _ -> Kernel_function.Hptset.singleton kf)
               user)
        in
        List.iter process_element users
      in
      List.iter process_callstack callstacks
  in
  Globals.Functions.iter process;
  Users.mark_as_computed ()

let add_eva_hook () =
  Eva.Analysis.(register_computation_hook ~on:Computed compute_users)

let init () = if ForceUsers.get () then add_eva_hook ()
let () = Cmdline.run_after_configuring_stage init

let get kf =
  let find kf =
    try Users.find kf
    with Not_found -> Kernel_function.Hptset.empty
  in
  if Users.is_computed () then
    find kf
  else begin
    if Eva.Analysis.is_computed () then begin
      feedback "requiring again the computation of the value analysis";
      Project.clear
        ~selection:(State_selection.with_dependencies Eva.Analysis.self)
        ()
    end else
      feedback ~level:2 "requiring the computation of the value analysis";
    Eva.Analysis.compute ();
    compute_users ();
    find kf
  end

let print () =
  if ForceUsers.get () then
    result "@[<v>====== DISPLAYING USERS ======@ %t\
            ====== END OF USERS =========="
      (fun fmt ->
         Callgraph.Uses.iter_in_rev_order
           (fun kf ->
              let callees = get kf in
              if not (Kernel_function.Hptset.is_empty callees) then
                Format.fprintf fmt "@[<hov 4>%a: %a@]@ "
                  Kernel_function.pretty kf
                  (Pretty_utils.pp_iter
                     ~pre:"" ~sep:"@ " ~suf:"" Kernel_function.Hptset.iter
                     Kernel_function.pretty)
                  callees))

let print_once, _self_print =
  State_builder.apply_once "Users_register.print" [ Users.self ] print

let () = Boot.Main.extend print_once

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