package frama-c

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

Install 

dune-project
 Dependency

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

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. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module Frama_c_kernel.Project

Projects management.

A project groups together all the internal states of Frama-C. An internal state is roughly the result of a computation which depends of an AST. It is possible to have many projects at the same time. For registering a new state in the Frama-C projects, apply the functor State_builder.Register.

Types for project

include Datatype.S_no_copy with type t = Project_skeleton.t
include Datatype.Ty with type t = Project_skeleton.t
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

type project = private Project_skeleton.t = {
  1. pid : int;
  2. mutable name : string;
  3. mutable unique_name : string;
}

Type of a project.

Operations on all projects

val create : string -> t

Create a new project with the given name and attach it after the existing projects (so the current project, if existing, is unchanged). The given name may be already used by another project. If there is no other project, then the new one is the current one.

val register_create_hook : (t -> unit) -> unit

register_create_hook f adds a hook on function create: each time a new project p is created, f p is applied.

The order in which hooks are applied is the same than the order in which hooks are registered.

exception NoProject

May be raised by current.

val current : unit -> t

The current project.

val is_current : t -> bool

Check whether the given project is the current one or not.

val iter_on_projects : (t -> unit) -> unit

iteration on project starting with the current one.

val fold_on_projects : ('a -> t -> 'a) -> 'a -> 'a

folding on project starting with the current one.

  • since Boron-20100401
val find_all : string -> t list

Find all projects with the given name.

val clear_all : unit -> unit

Clear all the projects: all the internal states of all the projects are now empty (wrt the action registered with register_todo_after_global_clear and register_todo_after_clear.

Operations on one project

Most operations have one additional selection as argument. If it is specified, the operation is only applied on the states of the given selection on the given project. Beware that the project may become inconsistent if your selection is incorrect.

val get_name : t -> string

Project name. Two projects may have the same name.

val get_unique_name : t -> string
  • returns

    a project name based on name but different of each others unique_name.

val set_name : t -> string -> unit

Set the name of the given project.

  • since Boron-20100401
exception Unknown_project
val from_unique_name : string -> t

Return a project based on unique_name.

val set_current : ?on:bool -> ?selection:State_selection.t -> t -> unit

Set the current project with the given one. The flag on is not for casual users.

val register_after_set_current_hook : user_only:bool -> (t -> unit) -> unit

register_after_set_current_hook f adds a hook on function set_current. The project given as argument to f is the old current project.

  • If user_only is true, then each time set_current is directly called by an user of this library, f () is applied.
  • If user_only is false, then each time set_current is applied (even indirectly through Project.on), f () is applied. The order in which each hook is applied is unspecified.
val on : ?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b

on p f x sets the current project to p, computes f x then restores the current project. You should use this function if you use a project different of current ().

val set_keep_current : bool -> unit

set_keep_current b keeps the current project forever (even after the end of the current on) iff b is true.

  • since Aluminium-20160501
val copy : ?selection:State_selection.t -> ?src:t -> t -> unit

Copy a project into another one. Default project for src is current (). Replace the destination by src. For each state to copy, the function copy given at state registration time must be fully implemented.

val create_by_copy : ?selection:State_selection.t -> ?src:t -> last:bool -> string -> t

Return a new project with the given name by copying some states from the project src. All the other states are initialized with their default values. Use the save/load mechanism for copying. Thus it does not require that the copy function of the copied state is implemented. All the hooks applied when loading a project are applied (see load). If last, then remember that the returned project is the last created one.

val create_by_copy_hook : (t -> t -> unit) -> unit

Register a hook to call at the end of create_by_copy. The first argument of the registered function is the copy source while the second one is the created project.

val clear : ?selection:State_selection.t -> ?project:t -> unit -> unit

Clear the given project. Default project is current (). All the internal states of the given project are now empty (wrt the action registered with register_todo_before_clear).

val register_todo_before_clear : (t -> unit) -> unit

Register an action performed just before clearing a project.

  • since Boron-20100401
val register_todo_after_clear : (t -> unit) -> unit

Register an action performed just after clearing a project.

  • since Boron-20100401
exception Cannot_remove of string

Raised by remove

val remove : ?project:t -> unit -> unit

Default project is current (). If the current project is removed, then the new current project is the previous current project if it still exists (and so on).

val register_before_remove_hook : (t -> unit) -> unit

register_before_remove_hook f adds a hook called just before removing a project.

  • since Beryllium-20090902

Inputs/Outputs

exception IOError of string
val save : ?compress:bool -> ?selection:State_selection.t -> ?project:t -> Filepath.t -> unit

Save a given project in a file. Default project is current ().

  • raises IOError

    if the project cannot be saved.

val load : ?selection:State_selection.t -> ?name:string -> Filepath.t -> t

Load a file into a new project given by its name. More precisely, load only except name file:

  1. creates a new project;
  2. performs all the registered before_load actions;
  3. loads the (specified) states of the project according to its description; and
  4. performs all the registered after_load actions.
  • raises IOError

    if the project cannot be loaded

  • returns

    the new project containing the loaded data.

val save_all : ?compress:bool -> ?selection:State_selection.t -> Filepath.t -> unit

Save all the projects in a file.

  • raises IOError

    a project cannot be saved.

val load_all : ?selection:State_selection.t -> Filepath.t -> unit

First remove all the existing project, then load all the projects from a file. For each project to load, the specification is the same than Project.load. Furthermore, after loading, all the hooks registered by register_after_set_current_hook are applied.

  • raises IOError

    if a project cannot be loaded.

val register_before_load_hook : (unit -> unit) -> unit

register_before_load_hook f adds a hook called just before loading **each project** (more precisely, the project exists and but is empty while the hook is applied): if n projects are on disk, the same hook will be called n times (one call by project).

Besides, for each project, the order in which the hooks are applied is the same than the order in which hooks are registered.

val register_after_load_hook : (unit -> unit) -> unit

register_after_load_hook f adds a hook called just after loading **each project**: if n projects are on disk, the same hook will be called n times (one call by project).

Besides, for each project, the order in which the hooks are applied is the same than the order in which hooks are registered.

val register_after_global_load_hook : (unit -> unit) -> unit

register_after_load_hook f adds a hook called just after loading **all projects**. f must not set the current project.

  • since Boron-20100401

Handling the selection

val get_current_selection : unit -> State_selection.t

If an operation on a project is ongoing, then get_current_selection () returns the selection which is applied on. The behaviour is unspecified if this function is called when no operation depending on a selection is ongoing.

Projects are comparable values

val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int

Undoing

module Undo : sig ... end