package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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_on_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 : ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.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.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.
  • raises IOError

    if the project cannot be loaded

  • returns

    the new project containing the loaded data.

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

Save all the projects in a file.

  • raises IOError

    a project cannot be saved.

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.

  • 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
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