Module Lmap_sig

module Lmap_sig: sig .. end

Signature for maps from bases to memory maps. The memory maps are intended to be those of the Offsetmap module.

type v

type of the values associated to a location

type offsetmap

type of the maps associated to a base

type widen_hint_base

widening hints for each base

module LBase: sig .. end

type tt = private

`\|`	`Bottom`
`\|`	`Top`
`\|`	`Map of LBase.t`

include Datatype.S_with_collections

type widen_hint = Base.Set.t * (Base.t -> widen_hint_base)

Bases that must be widening in priority, plus widening hints for each base.

val add_base : Base.t -> offsetmap -> t -> t

val pretty : Format.formatter -> t -> unit

val pretty_filter : Format.formatter -> t -> Locations.Zone.t -> unit

pretty_filter m z pretties only the part of m that correspond to the bases present in z

val pretty_diff : Format.formatter -> t -> t -> unit

val add_binding : with_alarms:CilE.warn_mode ->
       reducing:bool -> exact:bool -> t -> Locations.location -> v -> t

val find : with_alarms:CilE.warn_mode ->
       conflate_bottom:bool -> t -> Locations.location -> v

val join : t -> t -> t

val is_included : t -> t -> bool

val top : t

val is_top : t -> bool

val empty_map : t

Empty map. Casual users do not need this.

val is_empty_map : t -> bool

val bottom : t

Every location is associated to VALUE.bottom in bottom. This state can be reached only in dead code.

val is_reachable : t -> bool

val widen : widen_hint -> t -> t -> t

val filter_base : (Base.t -> bool) -> t -> t

Remove from the map all the bases that do not satisfy the predicate.

val filter_by_shape : 'a Hptmap.Shape(Base.Base).t -> t -> t

Remove from the map all the bases that are not also present in the given Base.t-indexed tree.

val find_base : Base.t -> t -> offsetmap

Raises Not_found if the varid is not present in the map.

val find_base_or_default : Base.t -> t -> offsetmap

val remove_base : Base.t -> t -> t

Removes the base if it is present. Does nothing otherwise.

val paste_offsetmap : with_alarms:CilE.warn_mode ->
       from:offsetmap ->
       dst_loc:Locations.Location_Bits.t ->
       start:Integer.t -> size:Integer.t -> exact:bool -> t -> t

paste_offsetmap ~from:offmap ~dst_loc ~start ~size ~exact m copies size bits starting at start in offmap, and pastes them at dst_loc in m. The copy is exact if and only if dst_loc is exact, and exact is true

val copy_offsetmap : with_alarms:CilE.warn_mode ->
       Locations.location -> t -> offsetmap option

copy_offsetmap alarms loc m returns the superposition of the bits pointed to by loc within m. loc.size must not be top. Return None if all pointed adresses are invalid in m.

val fold_base : (Base.t -> 'a -> 'a) -> t -> 'a -> 'a

fold_base f m calls f on all bases bound to non top offsetmaps in the non bottom map m.
Raises Error_Bottom if m is bottom.

val fold_base_offsetmap : (Base.t -> offsetmap -> 'a -> 'a) -> t -> 'a -> 'a

fold_base_offsetmap f m calls f on all bases bound to non top offsetmaps in the non bottom map m.
Raises Error_Bottom if m is bottom.

val add_new_base : Base.t -> size:Integer.t -> v -> size_v:Integer.t -> t -> t

exception Error_Bottom

Cached iterators

val cached_fold : f:(Base.t -> offsetmap -> 'a) ->
       cache_name:string ->
       temporary:bool -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a

val cached_map : f:(Base.t -> offsetmap -> offsetmap) ->
       cache:string * int -> temporary:bool -> t -> t

Prefixes. To be used by advanced users only

type subtree

val comp_prefixes : t -> t -> unit

val find_prefix : t -> Hptmap.prefix -> subtree option

val hash_subtree : subtree -> int

val equal_subtree : subtree -> subtree -> bool

exception Found_prefix of Hptmap.prefix * subtree * subtree

val clear_caches : unit -> unit

Clear the caches local to this module. Beware that they are not project-aware, and that you must call them at every project switch.