Frama-C API - Make_bitwise
Maps from intervals to simple values. The documentation of the returned maps is in module Offsetmap_bitwise_sig
.
Parameters
module V : sig ... end
Signature
type v = V.t
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
.
Pretty-printing
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
Join and inclusion testing
Finding values
val find : Int_Intervals_sig.itv -> t -> v
val find_iset : validity:Base.validity -> intervals -> t -> v
Adding values
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
Creating an offsetmap
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
.
Iterators
type map2_decide =
| ReturnLeft
| ReturnRight
| ReturnConstant of v
| 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
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.
Shape
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.