Previous  Up  Next

Module State

module State: sig .. end

A state is a project-compliant mutable value.

Type declarations

include Datatype.S_with_collections
module type Local = sig .. end

Operations on the local state required for registering a new state via State_builder.Register.

Getters and setters

val get_name : t -> string

Name of a state.

val set_name : t -> string -> unit

Set the name of the given state.

val get_unique_name : t -> string

Unique name of a state.

val unique_name_from_name : string -> string
val dummy : t

A dummy state.

val dummy_unique_name : string
val is_dummy : t -> bool
exception Unknown
val get : string -> t
val get_descr : t -> Structural_descr.pack
val add_hook_on_update : t -> (unit -> unit) -> unit

Add an hook which is applied each time the project library changes the local value of the state.

Internals

All this stuff should not be used outside of the Project library.

type state_on_disk = {
   on_disk_value : Stdlib.Obj.t;
   on_disk_computed : bool;
   on_disk_saved : bool;
   on_disk_digest : Stdlib.Digest.t;
} 
type private_ops = private {
   descr : Structural_descr.pack;
   create : Project_skeleton.project -> unit;
   remove : Project_skeleton.project -> unit;
   clear : Project_skeleton.project -> unit;
   clear_some_projects : (Project_skeleton.project -> bool) -> Project_skeleton.project -> bool;
   copy : Project_skeleton.project -> Project_skeleton.project -> unit;
   commit : Project_skeleton.project -> unit;
   update : Project_skeleton.project -> unit;
   on_update : (unit -> unit) -> unit;
   clean : unit -> unit;
   serialize : Project_skeleton.project -> state_on_disk;
   unserialize : Project_skeleton.project -> state_on_disk -> unit; (*
  • Raises Incompatible_datatype if state_on_disk is not compatible with the datatype expected by Frama-C's state
*)
} 
exception Incompatible_datatype of string
val dummy_state_on_disk : state_on_disk
val private_ops : t -> private_ops

State generators

val create : descr:Structural_descr.pack ->
       create:(Project_skeleton.project -> unit) ->
       remove:(Project_skeleton.project -> unit) ->
       clear:(Project_skeleton.project -> unit) ->
       clear_some_projects:((Project_skeleton.project -> bool) ->
                            Project_skeleton.project -> bool) ->
       copy:(Project_skeleton.project -> Project_skeleton.project -> unit) ->
       commit:(Project_skeleton.project -> unit) ->
       update:(Project_skeleton.project -> unit) ->
       on_update:((unit -> unit) -> unit) ->
       clean:(unit -> unit) ->
       serialize:(Project_skeleton.project -> state_on_disk) ->
       unserialize:(Project_skeleton.project -> state_on_disk -> unit) ->
       unique_name:string -> name:string -> t
val delete : t -> unit