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

type map

Maps from Base.t to Lmap_sig.offsetmap

type lmap = private

`\|`	`Bottom`
`\|`	`Top`
`\|`	`Map of map`

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

General shape

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

val is_reachable : t -> bool

Every location is associated to the value bottom of type v in this state. This state can be reached only in dead code.

Join and inclusion

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

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 widen : widen_hint -> t -> t -> t

val merge : into:t -> t -> t

merge ~into t adds all binding from t into into.

Finding values

val find : ?conflate_bottom:bool -> t -> Locations.location -> v

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

Raises 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 Lattice_bounds.or_top_bottom

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

val find_base_or_default : Base.t -> t -> offsetmap Lattice_bounds.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.

Binding variables

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.

Filters

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.

val replace_base : Base.substitution -> t -> t

replace_bases substitition map replaces some bases in map according to substitution. If substitution conflates different bases, the offsetmaps bound to these bases are joined.

Iterators

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

Cached iterators

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

Misc

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.