Module Cmdline

module Cmdline: sig .. end
Command line parsing.
Consult the Plugin Development Guide for additional details.


Stage configurations

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

type stage = 
| Early
| Extending
| Extended
| Exiting
| Loading
| Configuring
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.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val run_during_extending_stage : (unit -> unit) -> unit
Register an action to be executed during the extending stage.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val run_after_extended_stage : (unit -> unit) -> unit
Register an action to be executed at the end of the extended stage.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
type exit 
Since Beryllium-20090901
val nop : exit
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
exception Exit
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
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.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val run_after_loading_stage : (unit -> unit) -> unit
Register an action to be executed at the end of the loading stage.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
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
Consult the Plugin Development Guide for additional details.
val run_after_configuring_stage : (unit -> unit) -> unit
Register an action to be executed at the end of the configuring stage.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
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.
Since Carbon-20101201
Consult the Plugin Development Guide for additional details.
val protect : exn -> string
Messages for exceptions raised by Frama-C
Since Boron-20100401
val catch_at_toplevel : exn -> bool
Since Boron-20100401
Returns true iff the given exception is caught by the Frama-C toplevel.
val catch_toplevel_run : f:(unit -> unit) ->
quit:bool -> 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 in other cases. Set quit to true iff Frama-C must stop after running f.
Change in Boron-20100401: additional arguments. They are now labelled
Change in Fluorine-20130601+Dev: add the exception as argument of on_error.
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 run_normal_exit_hook : unit -> unit
Run all the hooks registered by Cmdline.at_normal_exit.
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
Change in Neon-20130301: add the exception as argument of the hook.
val run_error_exit_hook : exn -> unit
Run all the hooks registered by Cmdline.at_normal_exit.
Since Boron-20100401
Change in Neon-20130301: add the exception as argument.
val error_occurred : exn -> unit
Remember that an error occurred. So Cmdline.run_error_exit_hook will be called when Frama-C will exit.
Since Boron-20100401
Change in Neon-20130301: add the exception as argument, fix spelling.
val bail_out : unit -> 'a
Stop Frama-C with exit 0.
Since Boron-20100401

Special functions

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
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 (or the default project if None).
Since Beryllium-20090901
Change in Carbon-20101201
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
val use_cmdline_files : (string list -> unit) -> unit
What to do with the list of files put on the command lines.
Since Beryllium-20090601-beta1
module Group: sig .. end
val help : unit -> exit
Display the help of Frama-C
Since Beryllium-20090601-beta1
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.
Since Beryllium-20090601-beta1
Raises Invalid_argument if the same shortname is registered twice
type option_setting = 
| Unit of (unit -> unit)
| Int of (int -> unit)
| String of (string -> unit)
| String_list of (string list -> unit)
Since Beryllium-20090601-beta1
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.
Since Beryllium-20090601-beta1
Change in Carbon-20101201
Change in 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) Pervasives.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 -> 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 string
Since Carbon-20110201

Special parameters

Frama-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
Since Boron-20100401
val kernel_verbose_atleast_ref : (int -> bool) Pervasives.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