module Offsetmap_bitwise_sig:sig
..end
Offsetmap_bitwise
module, that implement efficient maps
from intervals to values.
Values are simpler than those of the Offsetmap_sig
module: given a value
v
bound to an interval i
, all sub-intervals of i
are implicitly also
bound to v
. If you need e.g. to extract the k-th bit of the interval to
retrieve a more precise value, you must use the Offsetmap
module
instead.
type
v
include Datatype.S
type
intervals
val pretty : t Pretty_utils.formatter
val pretty_generic : ?typ:Cil_types.typ ->
?pretty_v:(Format.formatter -> v -> unit) ->
?skip_v:(v -> bool) ->
?sep:string -> unit -> Format.formatter -> t -> unit
val pretty_debug : t Pretty_utils.formatter
val join : t -> t -> t
val is_included : t -> t -> bool
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 -> [ `Bottom | `Map of t ]
val add_binding_ival : validity:Base.validity ->
exact:bool ->
Ival.t ->
size:Int_Base.t -> v -> t -> [ `Bottom | `Map of t ]
val create : size:Integer.t -> v -> t
size
must be strictly greater than zero.val empty : t
val size_from_validity : Base.validity -> Integer.t Bottom.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
.val map : (v -> v) -> t -> t
type
map2_decide =
| |
ReturnLeft |
|||
| |
ReturnRight |
|||
| |
ReturnConstant of |
|||
| |
Recurse |
(* |
See the documentation of type
Offsetmap_sig.map2_decide | *) |
val map2 : Hptmap_sig.cache_type ->
(t -> t -> map2_decide) ->
(v ->
v -> v) ->
t -> t -> t
Offsetmap_sig.map2_on_values
.val fold : (intervals -> v -> 'a -> 'a) ->
t -> 'a -> 'a
val fold_fuse_same : (intervals -> v -> 'a -> 'a) ->
t -> 'a -> 'a
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
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.val single_interval_value : t -> v option
single_interval_value o
returns Some v
if o
contains a single
interval, to which v
is bound, and None
otherwise.val is_same_value : t -> v -> bool
is_same_value o v
is true if the offsetmap o
contains a single
binding to v
, or is the empty offsetmap.val clear_caches : unit -> unit