package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Low-level Builder
High-level Builders
1. References
2. Weak Hashtbl
3. Hashtables
4. References on a set
5. Queue
6. Array
7. Proxies
8. Counters
Generic functor to hashcons an arbitrary type
1. Useful operations

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

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-beta-Nickel.tar.gz

sha256=0c80dae8074fcb3f6a33d7a41faf9939a2a336478a8d2c79e20e2d7bab953735

doc/frama-c.kernel/Frama_c_kernel/State_builder/index.html

Module `Frama_c_kernel.State_builder`

State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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
  (Datatype : Datatype.S)
  (_ : State.Local with type t = Datatype.t)
  (_ : sig ... end) : 
  S with module Datatype = Datatype

Register(Datatype)(Local_state)(Info) registers a new state. Datatype represents the datatype of a state, Local_state explains how to deal with the client-side state and Info are additional required information.

High-level Builders

References

module type Ref = sig ... end

Output signature of Ref.

module Ref
  (Data : Datatype.S)
  (_ : sig ... 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. Note that get will raise Not_found if the stored data is None. Use get_option if you want to have access to the option.

module Option_ref
  (Data : Datatype.S)
  (_ : 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
  (Data : Datatype.S)
  (_ : 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 (_ : sig ... end) : Ref with type data = int

Build a reference on an integer.

module Zero_ref (_ : Info) : Ref with type data = int

Build a reference on an integer, initialized with 0.

module Bool_ref (_ : sig ... end) : Ref with type data = bool

Build a reference on a boolean.

module False_ref (_ : Info) : Ref with type data = bool

Build a reference on a boolean, initialized with false.

module True_ref (_ : Info) : Ref with type data = bool

Build a reference on a boolean, initialized with true.

module Float_ref (_ : sig ... 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
  (W : Weak.S)
  (_ : Datatype.S with type t = W.data)
  (_ : 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
  (Data : Datatype.S)
  (_ : 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. Note that the table is not saved on disk.

module type Hashconsing_tbl =
  functor (Data : sig ... end) ->
  functor (_ : 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. Note that the resulting table is not saved on disk.

module Hashconsing_tbl_not_weak : Hashconsing_tbl

Hash table for hashconsing, but the internal table is _not_ weak (it is a regular hash table). This module should be used only in case perfect reproducibility matters, as the table will never be emptied by the GC.

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 Datatype.Make_input.rehash)

type ('k, 'v) hashtbl_event =

| Update of 'k * 'v
(*
A binding in the hashtable has been added or modified.
*)
| Remove of 'k
(*
A binding in the hashtable has been removed.
*)
| Clear
(*
The hashtable has been cleared.
*)

Events emitted when an Hashtbl state changes.

module type Hashtbl = sig ... end

Output signature of builders of hashtables.

module Hashtbl
  (H : Datatype.Hashtbl)
  (Data : Datatype.S)
  (_ : Info_with_size) : 
  Hashtbl
    with type key = H.key
     and type data = Data.t
     and module Datatype = H.Make(Data)

module Int_hashtbl
  (Data : Datatype.S)
  (_ : 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
  (S : Datatype.Set)
  (_ : Info) : 
  Set_ref with type elt = S.elt and type data = S.t

Queue

module type Queue = sig ... end

module Queue (Data : Datatype.S) (_ : Info) : Queue with type elt = Data.t

Array

module type Array = sig ... end

module Array
  (Data : Datatype.S)
  (_ : sig ... end) : 
  Array with type elt = Data.t

Proxies

module Proxy : sig ... end

State proxy. A proxy is a state which does not correspond to any useful mutable value. Its goal is only to reduce the number of dependencies between groups of states.

Counters

module type Counter = sig ... end

module SharedCounter (_ : sig ... end) : Counter

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

module Counter (_ : sig ... end) : Counter

Creates a projectified counter. That starts at 0

Generic functor to hashcons an arbitrary type

module type Hashcons = sig ... end

Output signature of Hashcons below.

module Hashcons
  (Data : Datatype.S)
  (_ : sig ... 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