Frama-C:
Plug-ins:
Libraries:

Frama-C API - Lmap

Maps from bases to memory maps. The memory maps are those of the Offsetmap module.

type 'a default_contents =
  1. | Bottom
  2. | Top of 'a
  3. | Constant of 'a
  4. | Other

Contents of a variable when it is not present in the state. See function default_contents in the signature below

module type Default_offsetmap = sig ... end
module Make_LOffset (V : sig ... end) (Offsetmap : Offsetmap_sig.S with type v = V.t and type widen_hint = V.widen_hint) (_ : Default_offsetmap with type v := V.t and type offsetmap := Offsetmap.t) : Lmap_sig.S with type v = V.t and type widen_hint_base = V.widen_hint and type offsetmap = Offsetmap.t