Frama-C:
Plug-ins:
Libraries:

Frama-C API - States

Synchronized values between Server and Client

type 'a callback = ('a -> unit) -> unit
val register_hook : Request.signal -> 'a callback -> unit

Connect a hook registry to a signal. As soon as the signal is being traced, a hook to emit the signal is registered.

val register_value : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> output:'a Request.output -> get:(unit -> 'a) -> ?add_hook:'b callback -> unit -> Request.signal

Register a (projectified) value and generates the associated signal and request:

  • Signal <name>.sig is emitted on value updates;
  • GET Request <name>.get returns the current value.

If provided, the ~add_hook option is used to register a hook to notify the server of value updates. The hook will be installed only once the client starts to listen for value updates.

Inside Ivette you can use the States.useSyncValue(id) hook to synchronize with this value.

module type Value = sig ... end

Sub-signature of State_builder.Ref for register_framac_value.

val register_framac_value : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> output:'a Request.output -> (module Value with type data = 'a) -> Request.signal

Same as register_value but takes a State_builder.Ref module as parameter.

val register_state : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> data:'a Data.data -> get:(unit -> 'a) -> set:('a -> unit) -> ?add_hook:'b callback -> unit -> Request.signal

Register a (projectified) state and generates the associated signal and requests:

  • Signal <name>.sig is emitted on value updates;
  • GET Request <name>.get returns the current value;
  • SET Request <name>.set modifies the server value.

If provided, the ~add_hook option is used to register a hook to notify the server of value updates. The hook will be installed only once the client starts to listen for value updates.

Inside Ivette you can use the States.useSyncState(id) hook to synchronize with this state.

module type State = sig ... end

Sub-signature of State_builder.Ref for register_framac_state.

val register_framac_state : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> data:'a Data.data -> (module State with type data = 'a) -> Request.signal

Same as register_state but takes a State_builder.Ref module as parameter.

type 'a model

Columns array model

val model : unit -> 'a model

Creates an empty array model.

val column : name:string -> descr:Frama_c_kernel.Markdown.text -> data:'b Request.output -> get:('a -> 'b) -> ?default:'b -> 'a model -> unit

Populate an array model with a new field. If a ~default value is given, the field becomes optional and the field is omitted when equal to the default value (compared with =).

val option : name:string -> descr:Frama_c_kernel.Markdown.text -> data:'b Request.output -> get:('a -> 'b option) -> 'a model -> unit

Populate an array model with a new optional field.

type 'a array

Synchronized array state.

val reload : 'a array -> unit

Mark the array to be fully reloaded.

val update : 'a array -> 'a -> unit

Mark an array entry as updated.

val remove : 'a array -> 'a -> unit

Mark an array entry as removed.

val signal : 'a array -> Request.signal

Get the signal associated with the array.

val register_array : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> key:('a -> string) -> ?keyName:string -> ?keyType:Package.jtype -> iter:'a callback -> ?preload:('a -> unit) -> ?add_update_hook:'a callback -> ?add_remove_hook:'a callback -> ?add_reload_hook:unit callback -> 'a model -> 'a array

Register everything necessary to synchronize an array with the client:

  • Signal <name>.sig is emitted on array updates;
  • GET Request <name>.fetch is registered to get updates;
  • GET Request <name>.reload is registered to trigger a full reload.

The ~key parameter is used to identify array entries, and used to fill the reserved column "id" of entries.

Columns added to the model after registration are not taken into account.

The optional ~preload function will be called just before every column getters. Notice that column getters are called in registration order.

If provided, the ~add_xxx_hook options are used to register hooks to notify the server of corresponding array updates. Each hook will be installed only once the client starts to listen for array updates.

Inside Ivette you can obtain the entries in sync by using the States.useSyncArray() hook.

module type TableState = sig ... end

Sub-signature of State_builder.Hashtbl for register_framac_array.

val register_framac_array : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> key:('k -> string) -> ?keyName:string -> ?keyType:Package.jtype -> ('k * 'd) model -> (module TableState with type data = 'd and type key = 'k) -> ('k * 'd) array

Same as register_array but takes a State_builder.Hashtbl module as parameter.