Module Frama_c_kernel.Lmap

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

type 'a default_contents =
| Bottom
| Top of 'a
| Constant of 'a
| Other

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

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