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
type
map
Maps from Base.t
to Lmap_sig.offsetmap
type
lmap = private
| |
Bottom |
| |
Top |
| |
Map of |
include Datatype.S_with_collections
val pretty : Stdlib.Format.formatter -> t -> unit
val pretty_debug : Stdlib.Format.formatter -> t -> unit
val pretty_filter : Stdlib.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 : Stdlib.Format.formatter -> t -> t -> unit
val top : t
val is_top : t -> bool
val empty_map : t
Empty map. Casual users do not need this except to create a custom initial state.
val is_empty_map : t -> bool
val bottom : t
Every location is associated to the value bottom
of type v
in this
state. This state can be reached only in dead code.
val is_reachable : t -> bool
val join : t -> t -> t
val is_included : t -> t -> bool
module Make_Narrow:functor (
X
:
sig
include Lattice_type.With_Top
include Lattice_type.With_Narrow
val bottom_is_strict :bool
end
) ->
sig
..end
typewiden_hint =
Base.Set.t * (Base.t -> widen_hint_base)
Bases that must be widening in priority, plus widening hints for each base.
val widen : widen_hint -> t -> t -> t
val merge : into:t -> t -> t
merge ~into t
adds all binding from t
into into
.
val find : ?conflate_bottom:bool -> t -> Locations.location -> v
Error_Top
when the location or the state are Top, and there
is no Top value in the type Lmap_sig.v
.val copy_offsetmap : Locations.Location_Bits.t ->
Integer.t -> t -> offsetmap Bottom.or_bottom
copy_offsetmap alarms loc size m
returns the superposition of the
ranges of size
bits starting at loc
within m
. size
must be
strictly greater than zero. Return None
if all pointed addresses are
invalid in m
.
Error_Top
when the location or the state are Top, and there
is no Top value in the type Lmap_sig.v
.val find_base : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom
Not_found
if the varid is not present in the map.val find_base_or_default : Base.t -> t -> offsetmap Bottom.Top.or_top_bottom
Same as find_base
, but return the default values for bases
that are not currently present in the map. Prefer the use of this function
to find_base
, unless you explicitly want to see if the base is bound.
val add_binding : exact:bool -> t -> Locations.location -> v -> t
add_binding ~exact initial_mem loc v
simulates the effect of
writing v
at location loc
, in the initial memory state given by
initial_mem
.
If loc
is not writable, Lmap_sig.bottom
is returned.
If exact
is true, and loc
is a precise location, a strong update
is performed.
Only locations that may be valid are written.
Returns the resulting memory after the write.
val paste_offsetmap : from:offsetmap ->
dst_loc:Locations.Location_Bits.t -> size:Integer.t -> exact:bool -> t -> t
paste_offsetmap ~from ~dst_loc ~size ~exact m
copies from
, which is supposed to be exactly size
bits, and pastes
them at dst_loc
in m
. The copy is exact if and only if
dst_loc
is exact, and exact
is true. Only the locations that
may be valid are written.
val add_base : Base.t -> offsetmap -> t -> t
add_base b o m
adds base b
bound to o
, replacing any
previous bindings of b
. No effect on Top
or Bottom
.
val add_base_value : Base.t -> size:Integer.t -> v -> size_v:Integer.t -> t -> t
Creates the offsetmap described by size
, v
and size_v
,
and binds it to the base. No effect on Top
or Bottom
.
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 remove_base : Base.t -> t -> t
Removes the base if it is present. Does nothing otherwise.
Notice that some iterators require an argument of type Lmap_sig.map
: the
cases Top
and Bottom
must be handled separately. All the iterators
below only present bases that are bound to non-default values, according
to the function is_default_offsetmap
of the function Lmap.Make_Loffset
.
val iter : (Base.base -> offsetmap -> unit) -> map -> unit
val fold : (Base.t -> offsetmap -> 'a -> 'a) -> map -> 'a -> 'a
These functions are meant to be partially applied to all their arguments but the final one (the map). They must be called at the toplevel of OCaml modules, as they create persistent caches.
val cached_fold : f:(Base.t -> offsetmap -> 'a) ->
cache_name:string ->
temporary:bool -> joiner:('a -> 'a -> 'a) -> empty:'a -> map -> 'a
val cached_map : f:(Base.t -> offsetmap -> offsetmap) ->
cache:string * int -> temporary:bool -> t -> t
val remove_variables : Cil_types.varinfo list -> t -> t
val shape : map -> offsetmap Hptmap.Shape(Base.Base).t
Shape of the map. This can be used for simultaneous iterations
on other maps indexed by type Base.Base.t
.
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.