Previous  Up  Next

Module Project

module Project: sig .. end
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.
Consult the Plugin Development Guide for additional details.


Types for project


include Datatype.S_no_copy
module Datatype: Datatype.S_with_collections  with type t = Project_skeleton.t
type project = private Project_skeleton.t = private {
   pid : int;
   mutable name : string;
   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.
Raises NoProject if there is no project.
Consult the Plugin Development Guide for additional details.
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 Project.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.
Raises Unknown_project if no project has this unique name.
Change in Sodium-20150201
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.
Raises Invalid_argument if the given project does not exist anymore.
Consult the Plugin Development Guide for additional details.
val register_after_set_current_hook : user_only:bool -> (t -> unit) -> unit
register_after_set_current_hook f adds a hook on function Project.set_current. The project given as argument to f is the old current project. 
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 ().
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
Consult the Plugin Development Guide for additional details.
val set_keep_current : bool -> unit
set_keep_current b keeps the current project forever (even after the end of the current Project.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.
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
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 Project.load). If last, then remember that the returned project is the last created one (see last_created_by_copy).
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
Change in Sodium-20150201: add the labeled argument last.
val create_by_copy_hook : (t -> t -> unit) -> unit
Register a hook to call at the end of Project.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_on_clear).
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
Consult the Plugin Development Guide for additional details.
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).
Raises Cannot_remove if there is only one project.
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 : ?selection:State_selection.t -> ?project:t -> string -> unit
Save a given project in a file. Default project is current ().
Raises IOError if the project cannot be saved.
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
Consult the Plugin Development Guide for additional details.
val load : ?selection:State_selection.t -> ?name:string -> string -> 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.
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
Consult the Plugin Development Guide for additional details.
val save_all : ?selection:State_selection.t -> string -> unit
Save all the projects in a file.
Raises IOError a project cannot be saved.
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
val load_all : ?selection:State_selection.t -> string -> 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.
Change in Carbon-20101201: replace the optional arguments only and except by a single one selection.
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