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 (*
Initial stage for very specific almost hard-coded options. Do not use it.
Consult the Plugin Development Guide for additional details.
*)
| Extending (*
Before loading plug-ins. Run only once.
Consult the Plugin Development Guide for additional details.
*)
| 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").
Consult the Plugin Development Guide for additional details.
*)
| Exiting (*
Run once when exiting Frama-C.
Consult the Plugin Development Guide for additional details.
*)
| 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).
Consult the Plugin Development Guide for additional details.
*)
| 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.
Consult the Plugin Development Guide for additional details.
*)
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 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
Change in Neon-20130301: add the exception as argument of the hook.
module Group: sig .. end
Group of command line options.