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

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