Frama-C:
Plug-ins:
Libraries:

Frama-C API - Hptmap_sig

Signature for the Hptmap module

Functions on hptmaps are divided into two module types:

  • Shape contains only functions that do not create or modify a map: comparisons, tests, finding an element or a key, iterators.
  • S includes Shape, plus functions that create and modify maps: adding or removing elements, filter and maps, merge of two maps.
type cache_type =
  1. | NoCache
    (*

    The results of the function will not be cached.

    *)
  2. | PersistentCache of string
    (*

    The results of the function will be cached, and the function that uses the cache is a permanent closure (at the toplevel of an OCaml module).

    *)
  3. | TemporaryCache of string
    (*

    The results of the function will be cached, but the function itself is a local function which is garbage-collectable.

    *)

Some functions of this module may optionally use internal caches. It is the responsibility of the use to choose whether or not to use a cache, and whether this cache will be garbage-collectable by OCaml.

module type Shape = sig ... end

This module type contains only functions that do not create or modify maps. These functions can be applied to any maps from a given type key, regardless of the type of values bound.

module type S = sig ... end

Signature for hptmaps from hash-consed trees to values.