cmdline.mli 15.3 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
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
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(** Command line parsing. 
    @plugin development guide *)

(* ************************************************************************** *)
(** {2 Stage configurations}
(* ************************************************************************** *)

    Frama-C uses several stages for parsing its command line.
    Each of them may be customized. *)

type stage =
  | Early       (** Initial stage for very specific almost hard-coded
                    options. Do not use it.
                    @plugin development guide *)
  | Extending   (** Before loading plug-ins. Run only once.
                    @plugin development guide *)
  | Extended    (** The stage where plug-ins are loaded.
                    It is also the first stage each time the Frama-C main
                    loop is run (e.g. after each "-then").
                    @plugin development guide *)
  | Exiting     (** Run once when exiting Frama-C.
                    @plugin development guide *)
  | Loading     (** After {!Extended}, the stage where a previous Frama-C
                    internal states is restored (e.g. the one specified by
                    -load or by running the journal).
                    @plugin development guide *)
  | Configuring (** The stage where all the parameters which were not already
                    set may be modified to take into account cmdline options.
                    Just after this stage, Frama-C will run the plug-in mains.
                    @plugin development guide *)
    (** The different stages, from the first to be executed to the last one.
        @since Beryllium-20090601-beta1 *)

val run_after_early_stage: (unit -> unit) -> unit
  (** Register an action to be executed at the end of the early stage.
      @plugin development guide
      @since Beryllium-20090901 *)

val run_during_extending_stage: (unit -> unit) -> unit
  (** Register an action to be executed during the extending stage.
      @plugin development guide
      @since Beryllium-20090901 *)

val run_after_extended_stage: (unit -> unit) -> unit
  (** Register an action to be executed at the end of the extended stage.
      @plugin development guide
      @since Beryllium-20090901 *)

type exit
  (** @since Beryllium-20090901 *)

val nop : exit
  (** @since Beryllium-20090901
      @plugin development guide *)

exception Exit
  (** @since Beryllium-20090901
      @plugin development guide *)

val run_after_exiting_stage: (unit -> exit) -> unit
  (** Register an action to be executed at the end of the exiting stage.
      The guarded action must finish by [exit n].
      @plugin development guide
      @since Beryllium-20090601-beta1 *)

val run_after_loading_stage: (unit -> unit) -> unit
  (** Register an action to be executed at the end of the loading stage.
      @plugin development guide
      @since Beryllium-20090601-beta1 *)

val is_going_to_load: unit -> unit
  (** To be call if one action is going to run after the loading stage.
      It is not necessary to call this function if the running action is set by
      an option put on the command line.
      @since Beryllium-20090601-beta1
      @plugin development guide *)

val run_after_configuring_stage: (unit -> unit) -> unit
  (** Register an action to be executed at the end of the configuring stage.
      @plugin development guide
      @since Beryllium-20090601-beta1 *)

val run_after_setting_files: (string list -> unit) -> unit
(** Register an action to be executed just after setting the files put on the
    command line. The argument of the function is the list of files.
    @plugin development guide
    @since Carbon-20101201 *)

val at_normal_exit: (unit -> unit) -> unit
  (** Register a hook executed whenever Frama-C exits without error (the exit
      code is 0).
      @since Boron-20100401 *)

val at_error_exit: (exn -> unit) -> unit
  (** Register a hook executed whenever Frama-C exits with error (the exit
      code is greater than 0). The argument of the hook is the exception at the
      origin of the error.
      @since Boron-20100401
      @modify Neon-20130301 add the exception as argument of the
      hook. *)

(** Group of command line options.
    @since Beryllium-20090901 *)
module Group : sig
  type t (** @since Beryllium-20090901 *)
  val default: t (** @since Beryllium-20090901 *)
  val name: t -> string
    (** @since Beryllium-20090901 *)

  (**/**)
  (** Kernel internals *)

  val add: ?memo:bool -> plugin:string -> string -> t * bool
    (** Add a new group of options to the given plugin.
        If [memo] is [true], just return the already registered group if any.
        If [memo] is [false], cannot add twice a group with the same name.
        @return the group corresponding to the given name. Also return [true]
        iff the group has just been created.
        @since Beryllium-20090901 *)
  (**/**)

end

(**/**)

(* ************************************************************************** *)
(* ************************************************************************** *)
(** From here: functions required by Kernel Internals only! 
    You should not use them! *)
(* ************************************************************************** *)
(* ************************************************************************** *)

(* ************************************************************************** *)
(** {2 Handle Hooks} *)
(* ************************************************************************** *)

val protect: exn -> string
  (** Messages for exceptions raised by Frama-C
      @since Boron-20100401 *)

val catch_at_toplevel: exn -> bool
(** @return true iff the given exception is caught by the Frama-C toplevel.
    @since Boron-20100401 *)

val catch_toplevel_run:
  f:(unit -> unit) ->
  at_normal_exit:(unit -> unit) ->
  on_error:(exn -> unit) ->
  unit
    (** Run [f]. When done, either call [at_normal_exit] if running [f] was ok;
        or call [on_error] (and exits) in other cases.
        @modify Boron-20100401  additional arguments. They are now
        labelled
	@modify Neon-20140301 add the exception as argument of
	[on_error].
        @modify Magnesium-20151001 Removed argument [~quit]
    *)

val run_normal_exit_hook: unit -> unit
  (** Run all the hooks registered by {!at_normal_exit}.
      @since Boron-20100401 *)

val run_error_exit_hook: exn -> unit
  (** Run all the hooks registered by {!at_normal_exit}.
      @since Boron-20100401
      @modify Neon-20130301 add the exception as argument. *)

val error_occurred: exn -> unit
  (** Remember that an error occurred.
      So {!run_error_exit_hook} will be called when Frama-C will exit.
      @since Boron-20100401
      @modify Neon-20130301 add the exception as argument, 
      fix spelling. *)

val bail_out: unit -> 'a
  (** Stop Frama-C with exit 0.
      @since Boron-20100401 *)

(* ************************************************************************** *)
(** {2 Special functions}
(* ************************************************************************** *)

    These functions should not be used by a standard plug-in developer. *)

type on_from_name = { on_from_name: 'a. string -> (unit -> 'a) -> 'a }

val parse_and_boot:
  on_from_name:on_from_name ->
  get_toplevel:(unit -> (unit -> unit) -> unit) ->
  play_analysis:(unit -> unit) -> unit
(** Not for casual users.
    [parse_and_boot on_from_name get_toplevel play] performs the
    parsing of the command line, then play the analysis with the good
    toplevel provided by [get_toplevel]. [on_from_name] is [Project.on] on the
    project corresponding to the given (unique) name.
    @since Beryllium-20090901
    @modify Carbon-20101201
    @modify Sodium-20150201 the first argument of the first functional is no
    more a string option, just a string
    @modify Aluminium-20160501 add labels and generalize the type of
    [on_from_name] *)

val nb_given_options: unit -> int
  (** Number of options provided by the user on the command line.
      Should not be called before the end of the command line parsing.
      @since Beryllium-20090601-beta1 *)

230
val use_cmdline_files: (Datatype.Filepath.t list -> unit) -> unit
231
232
233
234
235
236
237
238
239
240
241
  (** What to do with the list of files put on the command lines.
      @since Beryllium-20090601-beta1 *)

val help: unit -> exit
  (** Display the help of Frama-C
      @since Beryllium-20090601-beta1 *)

val list_plugins: unit -> exit
  (** Display the list of installed plug-ins 
      @since Magnesium-20151001 *)

242
243
val explain_cmdline : unit -> exit

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
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
val plugin_help: string -> exit
  (** Display the help of the given plug-in (given by its shortname).
      @since Beryllium-20090601-beta1 *)

val print_option_help: 
  Format.formatter -> plugin:string -> group:Group.t -> string -> unit
(** Pretty print the help of the option (given by its plug-in, its group and its
    name) in the provided formatter.
    @since Oxygen-20120901 *)

val add_plugin: ?short:string -> string -> help:string -> unit
  (** [add_plugin ~short name ~help] adds a new plug-in recognized by the
      command line of Frama-C. If the shortname is not specified, then the name
      is used as the shortname. By convention, if the name and the shortname
      are equal to "", then the register "plug-in" is the Frama-C kernel
      itself.
      @raise Invalid_argument if the same shortname is registered twice
      @since Beryllium-20090601-beta1 *)

(** @since Beryllium-20090601-beta1 *)
type option_setting =
  | Unit of (unit -> unit)
  | Int of (int -> unit)
  | String of (string -> unit)

val add_option:
  string ->
  plugin:string ->
  group:Group.t ->
  stage ->
  ?argname:string ->
  help:string ->
  visible:bool ->
  ext_help:(unit,Format.formatter,unit) format ->
  option_setting ->
  unit
    (** [add_option name ~plugin stage ~argname ~help setting]
        adds a new option of the given [name] recognized by the command line of
        Frama-C. If the [name] is the empty string, nothing is done.
        [plugin] is the shortname of the plug-in.
        [argname] is the name of the argument which can be used of the
        description [help]. Both of them are used by the help of the
        registered option. If [help] is [None], then the option is not shown
        in the help.
        @since Beryllium-20090601-beta1
        @modify Carbon-20101201 
	@modify Oxygen-20120901 change type of ~help and add ~visible. *)

val add_option_without_action:
  string ->
  plugin:string ->
  group:Group.t ->
  ?argname:string ->
  help:string ->
  visible:bool ->
  ext_help:(unit,Format.formatter,unit) format ->
  unit ->
  unit
(** Equivalent to [add_option] without option setting.
    Thus do not add the option to any stage of the command line...
    Thus should not be used by casual users ;-).
    @since Carbon-20101201 *)

val add_aliases:
  string ->
  plugin:string ->
  group:Group.t ->
311
312
  ?visible: bool ->
  ?deprecated: bool ->
313
314
315
316
317
  stage ->
  string list ->
  unit
(** [add_aliases orig plugin group aliases] adds a list of aliases to the given
    option name [orig].
318
319
    If [visible] is set to false, the aliases do not appear in help messages.
    If [deprecated] is set to true, the use of the aliases emits a warning.
320
    @Invalid_argument if an alias name is the empty string
321
    @since Carbon-20110201
322
    @modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
323
324
325
326
327
328

val replace_option_setting: 
  string -> plugin:string -> group:Group.t -> option_setting -> unit
(** Replace the previously registered option setting. 
    @since Sodium-20150201 *)

329
330
331
val replace_option_help:
  string -> plugin:string -> group:Group.t -> string -> unit
(** Replace the previously registered option help.
Andre Maroneze's avatar
Andre Maroneze committed
332
    @since 21.0-Scandium *)
333

334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
(* ************************************************************************** *)
(** {2 Special parameters}
(* ************************************************************************** *)

    Frama-c parameters depending on the command line argument and set at the
    very beginning of the Frama-C initialization.

    They should not be used directly by a standard plug-in developer. *)

module Kernel_log: Log.Messages
(** @since Neon-20140301 *)

(** @since Fluorine-20130401 *)
module type Level = sig
  val value_if_set: int option ref
  val get: unit -> int
  val set: int -> unit
end

module Debug_level: Level
(** @since Fluorine-20130401 *)

module Verbose_level: Level
(** @since Fluorine-20130401 *)

module Kernel_debug_level: Level
(** @since Fluorine-20130401 *)

module Kernel_verbose_level: Level
(** @since Fluorine-20130401 *)

val kernel_debug_atleast_ref: (int -> bool) ref
  (** @since Boron-20100401 *)

val kernel_verbose_atleast_ref: (int -> bool) ref
  (** @since Boron-20100401 *)

val journal_enable: bool
  (** @since Beryllium-20090601-beta1 *)

val journal_isset: bool
  (** -journal-enable/disable explicitly set on the command line.
      @since Boron-20100401 *)

val use_obj: bool
  (** @since Beryllium-20090601-beta1 *)

val use_type: bool
  (** @since Beryllium-20090601-beta1 *)

val quiet: bool
  (** Must not be used for something else that initializing values
      @since Beryllium-20090601-beta1 *)

val deterministic: bool
  (** Indicates that the plugins should strive to be as deterministic as
      possible in their outputs. Higher memory consumption or analysis time
      are acceptable, as reproducibility is more important.
      @since Aluminium-20160501 *)

394
395
396
val permissive: bool
  (** Downgrades some command-line errors to warnings, such as
      unknown option names and invalid values for some options
397
      (e.g. non-existent function names).
398

399
      @since 22.0-Titanium *)
400

401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
val last_project_created_by_copy: (unit -> string option) ref

val load_all_plugins: (unit -> unit) ref

val add_loading_failures: string -> unit
(** Add a package to the list of ocamlfind packages that have failed to be
    loaded.
    @since Silicon-20161101 *)

(**/**)

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