Module Frama_c_kernel.State_builder

State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information.

Low-level Builder

module type Info = sig ... end

Additional information required by State_builder.Register.

module type Info_with_size = sig ... end
module type S = sig ... end

Output signature of State_builder.Register.

module Register (Datatype : Datatype.S) (_ : State.Local with type t = Datatype.t) (_ : sig ... end) : S with module Datatype = Datatype

Register(Datatype)(Local_state)(Info) registers a new state. Datatype represents the datatype of a state, Local_state explains how to deal with the client-side state and Info are additional required information.

High-level Builders

References

module type Ref = sig ... end

Output signature of Ref.

module Ref (Data : Datatype.S) (_ : sig ... end) : Ref with type data = Data.t and type Datatype.t = Data.t ref
module type Option_ref = sig ... end

Output signature of Option_ref. Note that get will raise Not_found if the stored data is None. Use get_option if you want to have access to the option.

module Option_ref (Data : Datatype.S) (_ : Info) : Option_ref with type data = Data.t

Build a reference on an option.

module type List_ref = sig ... end

Output signature of ListRef.

module List_ref (Data : Datatype.S) (_ : Info) : List_ref with type data = Data.t list and type data_in_list = Data.t

Build a reference on a list.

module Int_ref (_ : sig ... end) : Ref with type data = int

Build a reference on an integer.

module Zero_ref (_ : Info) : Ref with type data = int

Build a reference on an integer, initialized with 0.

module Bool_ref (_ : sig ... end) : Ref with type data = bool

Build a reference on a boolean.

module False_ref (_ : Info) : Ref with type data = bool

Build a reference on a boolean, initialized with false.

module True_ref (_ : Info) : Ref with type data = bool

Build a reference on a boolean, initialized with true.

module Float_ref (_ : sig ... end) : Ref with type data = float

Build a reference on a float.

Weak Hashtbl

module type Weak_hashtbl = sig ... end

Output signature of builders of hashtables.

module Weak_hashtbl (W : Weak.S) (_ : Datatype.S with type t = W.data) (_ : Info_with_size) : Weak_hashtbl with type data = W.data

Build a weak hashtbl over a datatype Data from a reference implementation W.

Build a weak hashtbl over a datatype Data by using Weak.Make provided by the OCaml standard library. Note that the table is not saved on disk.

module type Hashconsing_tbl = functor (Data : sig ... end) -> functor (_ : Info_with_size) -> Weak_hashtbl with type data = Data.t

Signature for the creation of projectified hashconsing tables..

Weak hashtbl dedicated to hashconsing. Note that the resulting table is not saved on disk.

Hash table for hashconsing, but the internal table is _not_ weak (it is a regular hash table). This module should be used only in case perfect reproducibility matters, as the table will never be emptied by the GC.

Weak or non-weak hashconsing tables, depending on variable Cmdline.deterministic.

Hashtables

IMPORTANT: that is INCORRECT to use projectified hashtables if keys have a custom rehash function (see Datatype.Make_input.rehash)

type ('k, 'v) hashtbl_event =
  1. | Update of 'k * 'v
    (*

    A binding in the hashtable has been added or modified.

    *)
  2. | Remove of 'k
    (*

    A binding in the hashtable has been removed.

    *)
  3. | Clear
    (*

    The hashtable has been cleared.

    *)

Events emitted when an Hashtbl state changes.

module type Hashtbl = sig ... end

Output signature of builders of hashtables.

module Hashtbl (H : Datatype.Hashtbl) (Data : Datatype.S) (_ : Info_with_size) : Hashtbl with type key = H.key and type data = Data.t and module Datatype = H.Make(Data)
module Int_hashtbl (Data : Datatype.S) (_ : Info_with_size) : Hashtbl with type key = int and type data = Data.t

References on a set

module type Set_ref = sig ... end

Output signature of builders of references on a set.

module Set_ref (S : Datatype.Set) (_ : Info) : Set_ref with type elt = S.elt and type data = S.t

Queue

module type Queue = sig ... end
module Queue (Data : Datatype.S) (_ : Info) : Queue with type elt = Data.t

Array

module type Array = sig ... end
module Array (Data : Datatype.S) (_ : sig ... end) : Array with type elt = Data.t

Proxies

module Proxy : sig ... end

State proxy. A proxy is a state which does not correspond to any useful mutable value. Its goal is only to reduce the number of dependencies between groups of states.

Counters

module type Counter = sig ... end
module SharedCounter (_ : sig ... end) : Counter

Creates a counter that is shared among all projects, but which is marshalling-compliant.

module Counter (_ : sig ... end) : Counter

Creates a projectified counter. That starts at 0

Generic functor to hashcons an arbitrary type

module type Hashcons = sig ... end

Output signature of Hashcons below.

module Hashcons (Data : Datatype.S) (_ : sig ... end) : Hashcons with type elt = Data.t

Hashconsed version of an arbitrary datatype

Useful operations

val apply_once : string -> State.t list -> (unit -> unit) -> (unit -> unit) * State.t

apply_once name dep f returns a closure applying f only once and the state internally used. name and dep are respectively the name and the dependencies of the local state created by this function. Should be used partially applied. If f raises an exception, then it is considered as not applied.

module States : sig ... end