Frama-C API - Location_map_bitwise
include Datatype.S with type t = lmap
include Datatype.S_no_copy with type t = lmap
include Datatype.Ty with type t = lmap
type t = lmap
include Lattice_type.Bounded_Join_Semi_Lattice with type t := t
include Lattice_type.Join_Semi_Lattice with type t := t
datatype of element of the lattice
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
val bottom : t
smallest element
include Lattice_type.With_Top with type t := t
val top : t
largest element
module LOffset : Offsetmap_bitwise_sig.S with type v = v and type intervals = Int_Intervals.t
val is_empty : t -> bool
val is_bottom : t -> bool
val empty : t
val empty_map : map
val pretty_generic_printer : ?pretty_v:v Pretty_utils.formatter -> ?skip_v:(v -> bool) -> sep:string -> unit -> t Pretty_utils.formatter
val pretty_debug : t Pretty_utils.formatter
val add_binding : exact:bool -> t -> Locations.Zone.t -> v -> t
val add_binding_loc : exact:bool -> t -> Locations.location -> v -> t
val find : t -> Locations.Zone.t -> v Lattice_bounds.or_bottom
Iterators
val fold : (Locations.Zone.t -> v -> 'a -> 'a) -> map -> 'a -> 'a
The following fold_* functions, as well as map2
take arguments of type map
to force their user to handle the cases Top and Bottom explicitly.
fold f m
folds a function f
on the bindings in m
. Contiguous bits with the same value are merged into a single zone. Different bases are presented in different zones.
val fold_fuse_same : (Locations.Zone.t -> v -> 'a -> 'a) -> map -> 'a -> 'a
Same behavior as fold
, except if two non-contiguous ranges r1
and r2
of a given base are mapped to the same value. fold
will call its argument f
on each range successively (hence, in our example, on r1
and r2
separately). Conversely, fold_fuse_same
will call f
directly on r1 U r2
, U being the join on sets of intervals.
val fold_join_zone : both:(Int_Intervals.t -> LOffset.t -> 'a) -> conv:(Base.t -> 'a -> 'b) -> empty_map:(Locations.Zone.t -> 'b) -> join:('b -> 'b -> 'b) -> empty:'b -> Locations.Zone.t -> map -> 'b
fold_join_zone ~both ~conv ~empty_map ~join ~empty z m
folds over the intervals present in z
. When a base b
is present in both z
and m
, and bound respectively to itvs
and mb
, both itvs mb
is called. The results obtained for this base b
are then converted using conv
. If a sub-zone z'
is present in z
, but the corresponding bases are not bound in m
, empty_map z'
is called. All the sub-results (of type) 'b
are joined using join
. empty
is used when an empty map or sub-zone is encountered. It must be a neutral element for join
.
This function internally uses a cache, and must be partially applied to its named arguments. (This explains the somewhat contrived interface, in particular the fact that both
and conv
are not fused.)
val map2 : cache:Hptmap_sig.cache_type -> symmetric:bool -> idempotent:bool -> empty_neutral:bool -> (LOffset.t -> LOffset.t -> LOffset.map2_decide) -> (v -> v -> v) -> map -> map -> map
'map'-like function between two interval maps, implemented as a simultaneous descent in both maps. map2 ~cache ~symmetric ~idempotent ~empty_neutral decide_fast f m1 m2
computes the map containing k |-> f v_1 v_2
for all the keys k
present in either m1
or m2
. When a key is present, v_i
is the corresponding value in the map. When it is missing in one of the maps, a default value is generated. (See argument default
to functor Make_bitwise
below.)
symmetric
, idempotent
, empty_neutral
and decide_fast
are present for optimisation purposes, to avoid visiting some trees. If symmetric
holds, f v1 v2 = f v2 v1
must also holds. If idempotent
holds, f v v = v
must also holds. Similarly, if empty_neutral
holds, f v default = f default v = v
must hold. decide_fast
is called before visiting two subtrees, and can be used to stop the recursion early. See the documentation of Offsetmap_sig.map2_decide
.
Depending on the value of cache
, the results of this function will be cached.
Misc
val shape : map -> LOffset.t Hptmap.Shape(Base.Base).t