module Cmdline:sig
..end
Frama-C uses several stages for parsing its command line.
Each of them may be customized.
type
stage =
| |
Early |
| |
Extending |
| |
Extended |
| |
Exiting |
| |
Loading |
| |
Configuring |
val run_after_early_stage : (unit -> unit) -> unit
val run_during_extending_stage : (unit -> unit) -> unit
val run_after_extended_stage : (unit -> unit) -> unit
type
exit
val nop : exit
exception Exit
val run_after_exiting_stage : (unit -> exit) -> unit
exit n
.val run_after_loading_stage : (unit -> unit) -> unit
val is_going_to_load : unit -> unit
val run_after_configuring_stage : (unit -> unit) -> unit
val run_after_setting_files : (string list -> unit) -> unit
val protect : exn -> string
val catch_at_toplevel : exn -> bool
val catch_toplevel_run : f:(unit -> unit) ->
quit:bool -> at_normal_exit:(unit -> unit) -> on_error:(exn -> unit) -> unit
f
. When done, either call at_normal_exit
if running f
was ok;
or call on_error
in other cases.
Set quit
to true
iff Frama-C must stop after running f
.on_error
.val at_normal_exit : (unit -> unit) -> unit
val run_normal_exit_hook : unit -> unit
val at_error_exit : (exn -> unit) -> unit
val run_error_exit_hook : exn -> unit
Cmdline.at_normal_exit
.val error_occurred : exn -> unit
Cmdline.run_error_exit_hook
will be called when Frama-C will exit.val bail_out : unit -> 'a
These functions should not be used by a standard plug-in developer.
val parse_and_boot : (string option -> (unit -> unit) -> unit) ->
(unit -> (unit -> unit) -> unit) -> (unit -> unit) -> unit
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 (or the default project if
None
).val nb_given_options : unit -> int
val use_cmdline_files : (string list -> unit) -> unit
module Group:sig
..end
val help : unit -> exit
val plugin_help : string -> exit
val print_option_help : Format.formatter -> plugin:string -> group:Group.t -> string -> unit
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.Invalid_argument
if the same shortname is registered twicetype
option_setting =
| |
Unit of |
| |
Int of |
| |
String of |
| |
String_list of |
val add_option : string ->
plugin:string ->
group:Group.t ->
stage ->
?argname:string ->
help:string ->
visible:bool ->
ext_help:(unit, Format.formatter, unit) Pervasives.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.val add_option_without_action : string ->
plugin:string ->
group:Group.t ->
?argname:string ->
help:string ->
visible:bool ->
ext_help:(unit, Format.formatter, unit) Pervasives.format -> unit -> unit
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 ;-).val add_aliases : string ->
plugin:string ->
group:Group.t -> stage -> string list -> unit
add_aliases orig plugin group aliases
adds a list of aliases to the given
option name orig
.
@Invalid_argument if an alias name is the empty stringFrama-c parameters depending on the command line argument and set at the very beginning of the Frama-C initialisation.
They should not be used directly by a standard plug-in developer.
module Kernel_log:Log.Messages
module type Level =sig
..end
module Debug_level:Level
module Verbose_level:Level
module Kernel_debug_level:Level
module Kernel_verbose_level:Level
val kernel_debug_atleast_ref : (int -> bool) Pervasives.ref
val kernel_verbose_atleast_ref : (int -> bool) Pervasives.ref
val journal_enable : bool
val journal_isset : bool
val use_obj : bool
val use_type : bool
val quiet : bool