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
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.