Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cmdline

Command line parsing.

Stage configurations

(* ************************************************************************** *)

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

type stage =
  1. | Early
    (*

    Initial stage for very specific almost hard-coded options. Do not use it.

    *)
  2. | Extending
    (*

    Before loading plug-ins. Run only once.

    *)
  3. | 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").

    *)
  4. | Exiting
    (*

    Run once when exiting Frama-C.

    *)
  5. | 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).

    *)
  6. | 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.

    *)

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
val run_during_extending_stage : (unit -> unit) -> unit

Register an action to be executed during the extending stage.

  • since Beryllium-20090901
val run_after_extended_stage : (unit -> unit) -> unit

Register an action to be executed at the end of the extended stage.

  • since Beryllium-20090901
type exit
  • since Beryllium-20090901
val nop : exit
  • since Beryllium-20090901
exception Exit
  • since Beryllium-20090901
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
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
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
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
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
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
module Group : sig ... end

Group of command line options.