plugin.mli 7.29 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
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
(*    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).            *)
(*                                                                        *)
(**************************************************************************)


(** Special signature for Kernel services, whose messages are handled in
    an ad'hoc manner. Should not be of any use for a standard plug-in,
    who would rather rely on {!Plugin.S} below.
    @since Chlorine-20180501
    @plugin development guide
*)
module type S_no_log = sig

  val add_group: ?memo:bool -> string -> Cmdline.Group.t
  (** Create a new group inside the plug-in.
      The given string must be different of all the other group names of this
      plug-in if [memo] is [false].
      If [memo] is [true] the function will either create a fresh group or
      return an existing group of the same name in the same plugin.
      [memo] defaults to [false]
      @since Beryllium-20090901 *)

  module Help: Parameter_sig.Bool
  (** @deprecated since Oxygen-20120901 *)

  module Verbose: Parameter_sig.Int
  module Debug: Parameter_sig.Int

  (** Handle the specific `share' directory of the plug-in.
      @since Oxygen-20120901 *)
  module Share: Parameter_sig.Specific_dir

Michele Alberti's avatar
Michele Alberti committed
51
  (** Handle the specific `session' directory of the plug-in.
52
53
54
      @since Neon-20140301 *)
  module Session: Parameter_sig.Specific_dir

Michele Alberti's avatar
Michele Alberti committed
55
  (** Handle the specific `config' directory of the plug-in.
56
57
58
59
      @since Neon-20140301 *)
  module Config: Parameter_sig.Specific_dir

  val help: Cmdline.Group.t
Michele Alberti's avatar
Michele Alberti committed
60
61
  (** The group containing option -*-help.
      @since Boron-20100401 *)
62
63

  val messages: Cmdline.Group.t
Michele Alberti's avatar
Michele Alberti committed
64
65
  (** The group containing options -*-debug and -*-verbose.
      @since Boron-20100401 *)
66

67
68
69
70
71
72
73
  val add_plugin_output_aliases:
    ?visible:bool -> ?deprecated:bool -> string list -> unit
    (** Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log,
        -plugin-msg-key, and -plugin-warn-key.
        [add_plugin_output_aliases [alias]] adds the aliases -alias-help,
        -alias-verbose, etc.
        @since 18.0-Argon
74
        @modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
75
76
77
78
79
80
81
82
end

(** Provided plug-general services for plug-ins.
    @since Beryllium-20090601-beta1
    @modify Chlorine-20180501 removed programmatic access to [Debug_category]:
    managing categories is now entirely done by Log.Messages
    @plugin development guide *)
module type S = sig
Michele Alberti's avatar
Michele Alberti committed
83
84
  include Log.Messages
  include S_no_log
85
86
87
end

type plugin = private
Michele Alberti's avatar
Michele Alberti committed
88
89
90
91
  { p_name: string;
    p_shortname: string;
    p_help: string;
    p_parameters: (string, Typed_parameter.t list) Hashtbl.t }
92
(** @since Beryllium-20090901
93
    @modify 22.0-Titanium previously only "iterable" parameters were included,
94
95
                        now all parameters are.
*)
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

module type General_services = sig
  include S
  include Parameter_sig.Builder
end

(**/**)

val register_kernel: unit -> unit
(** Begin to register parameters of the kernel. Not for casual users.
      @since Beryllium-20090601-beta1 *)

(**/**)

(** Functors for registering a new plug-in. It provides access to several
    services.
    @plugin development guide *)
module Register
Michele Alberti's avatar
Michele Alberti committed
114
115
116
117
118
    (P: sig
       val name: string (** Name of the module. Arbitrary non-empty string. *)
       val shortname: string (** Prefix for plugin options. No space allowed. *)
       val help: string (** description of the module. Free-form text. *)
     end):
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
  General_services

val is_share_visible: unit -> unit
(** Make visible to the end-user the -<plug-in>-share option.
    To be called just before applying {!Register} to create plug-in services.
    @since Oxygen-20120901 *)

val is_session_visible: unit -> unit
(** Make visible to the end-user the -<plug-in>-session option.
    To be called just before applying {!Register} to create plug-in services.
    @since Neon-20140301 *)

val is_config_visible: unit -> unit
(** Make visible to the end-user the -<plug-in>-config option.
    To be called just before applying {!Register} to create plug-in services.
    @since Neon-20140301 *)

val plugin_subpath: string -> unit
(** Use the given string as the sub-directory in which the plugin files will
    be installed (ie. [share/frama-c/plugin_subpath]...). Relevant for
    directories [Share], [Session] and [Config] above.
    @since Neon-20140301 *)

val default_msg_keys: string list -> unit
(** Debug message keys set by default for the plugin.
    @since Silicon-20161101
    @deprecated since Chlorine-20180501 use directly functions from Log
     (add_debug_keys and del_debug_keys) to manage the default status of each
     category
Michele Alberti's avatar
Michele Alberti committed
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

(* ************************************************************************* *)
(** {2 Handling plugins} *)
(* ************************************************************************* *)

val get_from_shortname: string -> plugin
(** Get a plug-in from its shortname.
    @since Oxygen-20120901  *)

val get_from_name: string -> plugin
(** Get a plug-in from its name.
    @since Oxygen-20120901 *)

val is_present: string -> bool
(** Whether a plug-in already exists.
    Plugins are identified by their short name.
    @since Magnesium-20151001 *)

val get: string -> plugin
[@@ deprecated "Use Plugin.get_from_name"]
(** Get a plug-in from its name.
    @deprecated since Oxygen-20120901 *)

val iter_on_plugins: (plugin -> unit) -> unit
173
(** Iterate on each registered plug-in.
Michele Alberti's avatar
Michele Alberti committed
174
    @since Beryllium-20090901 *)
175

176
177
val fold_on_plugins: (plugin -> 'a -> 'a) -> 'a -> 'a
(** Fold [f] on each registered plug-in.
178
    @since 22.0-Titanium *)
179

180
181
182
183
184
185
(**/**)
(* ************************************************************************* *)
(** {2 Internal kernel stuff} *)
(* ************************************************************************* *)

val positive_debug_ref: int ref
Michele Alberti's avatar
Michele Alberti committed
186
(** @since Boron-20100401 *)
187
188
189
190
191
192
193
194
195
196
197
198
199
200

val session_is_set_ref: (unit -> bool) ref
val session_ref: (unit -> string) ref

val config_is_set_ref: (unit -> bool) ref
val config_ref: (unit -> string) ref

(**/**)

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