Memory.LOffset
type v = v
Type of the values stored in the offsetmap
Datatype for the offsetmap
include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
val descr : t Frama_c_kernel.Descr.t
Datatype descriptor.
val packed_descr : Frama_c_kernel.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 : (Frama_c_kernel.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 = Frama_c_kernel.Int_Intervals.t
val pretty : t Frama_c_kernel.Pretty_utils.formatter
val pretty_generic :
?typ:Frama_c_kernel.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 Frama_c_kernel.Pretty_utils.formatter
val find : Frama_c_kernel.Int_Intervals_sig.itv -> t -> v
val find_iset : validity:Frama_c_kernel.Base.validity -> intervals -> t -> v
val add_binding_intervals :
validity:Frama_c_kernel.Base.validity ->
exact:bool ->
intervals ->
v ->
t ->
t Frama_c_kernel.Lattice_bounds.or_bottom
val add_binding_ival :
validity:Frama_c_kernel.Base.validity ->
exact:bool ->
Frama_c_kernel.Ival.t ->
size:Frama_c_kernel.Int_Base.t ->
v ->
t ->
t Frama_c_kernel.Lattice_bounds.or_bottom
val create : size:Frama_c_kernel.Integer.t -> v -> t
size
must be strictly greater than zero.
val empty : t
offsetmap containing no interval.
val size_from_validity :
Frama_c_kernel.Base.validity ->
Frama_c_kernel.Integer.t Frama_c_kernel.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 Offsetmap_sig.map2_decide
val map2 :
Frama_c_kernel.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 ->
(Frama_c_kernel.Int_Intervals_sig.itv -> v -> 'a -> 'a) ->
Frama_c_kernel.Int_Intervals_sig.itv ->
t ->
'a ->
'a
See documentation of Offsetmap_sig.fold_between
.
val fold_join_itvs :
cache:Frama_c_kernel.Hptmap_sig.cache_type ->
(Frama_c_kernel.Integer.t -> Frama_c_kernel.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.