package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. L
    Loïc Correnson
  16. J
    Julien Crétin
  17. P
    Pascal Cuoq
  18. Z
    Zaynah Dargaye
  19. B
    Basile Desloges
  20. J
    Jean-Christophe Filliâtre
  21. P
    Philippe Herrmann
  22. M
    Maxime Jacquemin
  23. F
    Florent Kirchner
  24. A
    Alexander Kogtenkov
  25. R
    Remi Lazarini
  26. T
    Tristan Le Gall
  27. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Cmdline/index.html

Module Frama_c_kernel.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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct