Location_map_bitwise.LOffset
type v = v
Type of the values stored in the offsetmap
Datatype for the offsetmap
include Datatype.S
include Datatype.S_no_copy
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 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
.
type intervals = Int_Intervals.t
val pretty : t Pretty_utils.formatter
val pretty_generic :
?typ:Cil_types.typ ->
?pretty_v:( Stdlib.Format.formatter -> v -> unit ) ->
?skip_v:( v -> bool ) ->
?sep:string ->
unit ->
Stdlib.Format.formatter ->
t ->
unit
val pretty_debug : t Pretty_utils.formatter
val find : Int_Intervals_sig.itv -> t -> v
val find_iset : validity:Base.validity -> intervals -> t -> v
val add_binding_intervals :
validity:Base.validity ->
exact:bool ->
intervals ->
v ->
t ->
t Lattice_bounds.or_bottom
val add_binding_ival :
validity:Base.validity ->
exact:bool ->
Ival.t ->
size:Int_Base.t ->
v ->
t ->
t Lattice_bounds.or_bottom
val empty : t
offsetmap containing no interval.
val size_from_validity : Base.validity -> Integer.t Lattice_bounds.or_bottom
size_from_validity v
returns the size to be used when creating a new offsetmap for a base with validity v
. This is a convention that should be shared by all modules that create offsetmaps. Returns `Bottom
iff v
is Invalid
.
type map2_decide =
| ReturnLeft | |
| ReturnRight | |
| ReturnConstant of v | |
| Recurse | (* See the documentation of type |
val map2 :
Hptmap_sig.cache_type ->
( t -> t -> map2_decide ) ->
( v -> v -> v ) ->
t ->
t ->
t
See the documentation of function Offsetmap_sig
.map2_on_values.
Same behavior as fold
, except if two disjoint intervals r1
and r2
are mapped to the same value and boolean. In this case, fold
will call its argument f
on r1
, then on r2
. fold_fuse_same
will call it directly on r1 U r2
, where U is the join on sets of intervals.
val fold_itv :
?direction:[ `LTR | `RTL ] ->
entire:bool ->
( Int_Intervals_sig.itv -> v -> 'a -> 'a ) ->
Int_Intervals_sig.itv ->
t ->
'a ->
'a
See documentation of Offsetmap_sig
.fold_between.
val fold_join_itvs :
cache:Hptmap_sig.cache_type ->
( Integer.t -> Integer.t -> v -> 'a ) ->
( 'a -> 'a -> 'a ) ->
'a ->
intervals ->
t ->
'a
fold_join f join vempty itvs m
is an implementation of fold
that restricts itself to the intervals in itvs
. Unlike in fold
(where the equivalent of f
operates on an accumulator), f
returns a value on each sub-interval independently. The results are joined using joined
. vempty
is the value that must be returned on Int_Intervals.bottom
. This function uses a cache internally. Hence, it must be partially applied to its first three arguments. If you do not need a cache, use fold
instead.
val is_single_interval : t -> bool
is_single_interval o
is true if the offsetmap o
contains a single binding.
single_interval_value o
returns Some v
if o
contains a single interval, to which v
is bound, and None
otherwise.
is_same_value o v
is true if the offsetmap o
contains a single binding to v
, or is the empty offsetmap.