package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module `Frama_c_kernel.Hptmap`

Efficient maps from hash-consed trees to values, implemented as Patricia trees.

This implementation of big-endian Patricia trees follows Chris Okasaki's paper at the 1998 ML Workshop in Baltimore. Maps are implemented on top of Patricia trees. A tree is big-endian if it expects the key's most significant bits to be tested first.

type prefix

Undocumented. Needed for advanced users only

module type Id_Datatype = sig ... end

Type of the keys of the map.

module Shape (Key : Id_Datatype) : sig ... end

This functor builds Hptmap_sig.Shape for maps indexed by keys Key, which contains all functions on hptmap that do not create or modify maps.

module type Info = sig ... end

Required information for the correctness of the hptmaps.

module Make
  (Key : Id_Datatype)
  (V : Datatype.S)
  (_ : Info with type key := Key.t and type v := V.t) : 
  Hptmap_sig.S
    with type key = Key.t
     and type v = V.t
     and type 'v map = 'v Shape(Key).map
     and type prefix = prefix

This functor builds the complete module of maps indexed by keys Key to values V.

module type Compositional_bool = sig ... end

An additional boolean information is computed for each tree, by composing the boolean on the subtrees and the value information on each leaf.

module Make_with_compositional_bool
  (Key : Id_Datatype)
  (V : Datatype.S)
  (_ : Compositional_bool with type key := Key.t and type v := V.t)
  (_ : Info with type key := Key.t and type v := V.t) : 
  Hptmap_sig.S
    with type key = Key.t
     and type v = V.t
     and type 'v map = 'v Shape(Key).map
     and type prefix = prefix

This functor builds the complete module of maps indexed by keys Key to values V, with an additional boolean information maintained for each tree.