package frama-c
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567
doc/frama-c-server.core/Server/States/index.html
Module Server.States
Source
Synchronized values between Server and Client
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.
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.
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.
Columns 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.
Synchronized array state.
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.
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.