package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz
sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c-server.core/Server/States/index.html

Module Server.StatesSource

Synchronized values between Server and Client

Sourcetype 'a callback = ('a -> unit) -> unit
Sourceval 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.

Sourceval 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.

Sourcemodule type Value = sig ... end

Sub-signature of State_builder.Ref for register_framac_value.

Sourceval 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.

Sourceval 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.

Sourcemodule type State = sig ... end

Sub-signature of State_builder.Ref for register_framac_state.

Sourceval 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.

Sourcetype 'a model

Columns array model

Sourceval model : unit -> 'a model

Creates an empty array model.

Sourceval 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 =).

Sourceval 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.

Sourcetype 'a array

Synchronized array state.

Sourceval reload : 'a array -> unit

Mark the array to be fully reloaded.

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

Mark an array entry as updated.

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

Mark an array entry as removed.

Sourceval signal : 'a array -> Request.signal

Get the signal associated with the array.

Sourceval register_array : package:Package.package -> name:string -> descr:Frama_c_kernel.Markdown.text -> key:('a -> string) -> ?keyName:string -> ?keyType:Package.jtype -> iter:'a callback -> ?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.

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.

Sourcemodule type TableState = sig ... end

Sub-signature of State_builder.Hashtbl for register_framac_array.

Sourceval 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.