Previous  Up  Next

Module State_builder

module State_builder: sig .. end

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: 
functor (Datatype : Datatype.S) -> 
functor (Local_state : State.Local  with type t = Datatype.t) -> 
functor (Info : sig
include State_builder.Info
val unique_name : string
end) -> S  with module Datatype = Datatype

Register(Datatype)(State)(Info) registers a new state.

High-level Builders

References

module type Ref = sig .. end

Output signature of Ref.

module Ref: 
functor (Data : Datatype.S) -> 
functor (Info : sig
include State_builder.Info
val default : unit -> Data.t
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.

module Option_ref: 
functor (Data : Datatype.S) -> 
functor (Info : 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: 
functor (Data : Datatype.S) -> 
functor (Info : 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: 
functor (Info : sig
include State_builder.Info
val default : unit -> int
end) -> Ref  with type data = int

Build a reference on an integer.

module Zero_ref: 
functor (Info : Info) -> Ref  with type data = int

Build a reference on an integer, initialized with 0.

module Bool_ref: 
functor (Info : sig
include State_builder.Info
val default : unit -> bool
end) -> Ref  with type data = bool

Build a reference on a boolean.

module False_ref: 
functor (Info : Info) -> Ref  with type data = bool

Build a reference on a boolean, initialized with false.

module True_ref: 
functor (Info : Info) -> Ref  with type data = bool

Build a reference on a boolean, initialized with true.

module Float_ref: 
functor (Info : sig
include State_builder.Info
val default : unit -> float
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: 
functor (W : Stdlib.Weak.S) -> 
functor (Data : Datatype.S  with type t = W.data) -> 
functor (Info : Info_with_size) -> Weak_hashtbl  with type data = W.data

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

module Caml_weak_hashtbl: 
functor (Data : Datatype.S) -> 
functor (Info : Info_with_size) -> Weak_hashtbl  with type data = Data.t

Build a weak hashtbl over a datatype Data by using Weak.Make provided by the OCaml standard library.

module type Hashconsing_tbl = functor (Data : sig
include Datatype.S

The hashconsed datatype

val equal_internal : t -> t -> bool

Equality on the datatype internally used by the built table.

val hash_internal : t -> int

Hash function for datatype internally used by the built table.

val initial_values : t list

Pre-existing values stored in the built table and shared by all existing projects.

end) -> functor (Info : Info_with_size) -> Weak_hashtbl  with type data = Data.t

Signature for the creation of projectified hashconsing tables..

module Hashconsing_tbl_weak: Hashconsing_tbl

Weak hashtbl dedicated to hashconsing.

module Hashconsing_tbl_not_weak: Hashconsing_tbl

Hash table for hashconsing, but the internal table is _not_ weak (it is a regular hash table).

module Hashconsing_tbl: Hashconsing_tbl

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 Project.DATATYPE_OUTPUT.rehash)

module type Hashtbl = sig .. end

Output signature of builders of hashtables.

module Hashtbl: 
functor (H : Datatype.Hashtbl) -> 
functor (Data : Datatype.S) -> 
functor (Info : Info_with_size) -> Hashtbl  with type key = H.key and type data = Data.t
                                and module Datatype = H.Make(Data)
module Int_hashtbl: 
functor (Data : Datatype.S) -> 
functor (Info : 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: 
functor (S : Datatype.Set) -> 
functor (Info : Info) -> Set_ref  with type elt = S.elt and type data = S.t

Queue

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

Array

module type Array = sig .. end
module Array: 
functor (Data : Datatype.S) -> 
functor (Info : sig
include State_builder.Info
val default : Data.t
end) -> Array  with type elt = Data.t

Proxies

module Proxy: sig .. end

State proxy.

Counters

module type Counter = sig .. end
module SharedCounter: 
functor (Info : sig
val name : string
end) -> Counter

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

module Counter: 
functor (Info : sig
val name : string
end) -> Counter

Creates a projectified counter.

Generic functor to hashcons an arbitrary type 

module type Hashcons = sig .. end

Output signature of Hashcons below.

module Hashcons: 
functor (Data : Datatype.S) -> 
functor (Info : sig
include State_builder.Info
val initial_values : Data.t list

List of values created at compile-time, that must be shared between all instances of Frama-C.

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