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.

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.

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.

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
val set_name : t -> string -> unit

Set the name of the given project.

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 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 ().

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.

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 Project.load). If last, then remember that the returned project is the last created one (see last_created_by_copy).

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

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

Register an action performed just before clearing a project.

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

Register an action performed just after clearing a project.

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.

Inputs/Outputs

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

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

val load : ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.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.
val save_all : ?selection:State_selection.t -> Filepath.Normalized.t -> unit

Save all the projects in a file.

val load_all : ?selection:State_selection.t -> Filepath.Normalized.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.

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.

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