Module BO.ArrayBlk

module ArrInfo : sig ... end
include Absint.AbstractDomain.MapS with type key = AbsLoc.Allocsite.t and type value = ArrInfo.t
include IStdlib.PrettyPrintable.PPMonoMap
include IStdlib.PrettyPrintable.MonoMap
type key
type value
type t
val empty : t
val is_empty : t -> bool
val mem : key -> t -> bool
val add : key -> value -> t -> t
val update : key -> (value option -> value option) -> t -> t
val singleton : key -> value -> t
val remove : key -> t -> t
val merge : (key -> value option -> value option -> value option) -> t -> t -> t
val union : (key -> value -> value -> value option) -> t -> t -> t
val compare : (value -> value -> int) -> t -> t -> int
val equal : (value -> value -> bool) -> t -> t -> bool
val iter : (key -> value -> unit) -> t -> unit
val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (key -> value -> bool) -> t -> bool
val exists : (key -> value -> bool) -> t -> bool
val filter : (key -> value -> bool) -> t -> t
val partition : (key -> value -> bool) -> t -> t * t
val cardinal : t -> int
val bindings : t -> (key * value) list
val min_binding : t -> key * value
val min_binding_opt : t -> (key * value) option
val max_binding : t -> key * value
val max_binding_opt : t -> (key * value) option
val choose : t -> key * value
val choose_opt : t -> (key * value) option
val split : key -> t -> t * value option * t
val find : key -> t -> value
val find_opt : key -> t -> value option
val find_first : (key -> bool) -> t -> key * value
val find_first_opt : (key -> bool) -> t -> (key * value) option
val find_last : (key -> bool) -> t -> key * value
val find_last_opt : (key -> bool) -> t -> (key * value) option
val map : (value -> value) -> t -> t
val mapi : (key -> value -> value) -> t -> t
val is_singleton_or_more : t -> (key * value) IStdlib.IContainer.singleton_or_more
val fold_map : t -> init:'a -> f:('a -> value -> 'a * value) -> 'a * t
val of_seq : (key * value) Stdlib.Seq.t -> t
include IStdlib.PrettyPrintable.PrintableType with type t := t
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val pp_key : IStdlib.PrettyPrintable.F.formatter -> key -> unit
include Absint.AbstractDomain.WithBottom with type t := t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val bottom : t

The bottom value of the domain.

val is_bottom : t -> bool

Return true if this is the bottom value

val compare : t -> t -> int
val bot : t
val make_c : AbsLoc.Allocsite.t -> offset:Itv.t -> size:Itv.t -> stride:Itv.t -> t

Make an array block for C

val make_java : AbsLoc.Allocsite.t -> length:Itv.t -> t

Make an array block for Java

val unknown : t
val get_pow_loc : t -> AbsLoc.PowLoc.t

Return all allocsites as PowLoc.t

val is_bot : t -> bool
val is_symbolic : t -> bool

Check if there is a symbolic integer value in its offset or size

val lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> Boolean.t

Lift a comparison of Itv.t and Loc.t to that of t. The comparison for Itv.t is used for integer values such as offset and size, and the comparison for Loc.t is used for allocsites.

val transform_length : f:(Itv.t -> Itv.t) -> t -> t

Apply f to all sizes

val prune_binop : IR.Binop.t -> t -> t -> t

prune_binop bop x y returns a pruned value of x by bop and y.

val prune_eq : t -> t -> t

prune_eq x y returns a pruned value of x by == y.

val prune_ne : t -> t -> t

prune_ne x y returns a pruned value of x by != y.

val minus_offset : t -> Itv.t -> t
val plus_offset : t -> Itv.t -> t
val diff : t -> t -> Itv.t

Return difference of offsets between given array blocks

val normalize : t -> t

Normalize all interval values such as offset and size in it. Thus, if an interval value is invalid, the interval value is replaced with bottom.

val subst : t -> Bounds.Bound.eval_sym -> AbsLoc.PowLoc.eval_locpath -> AbsLoc.PowLoc.t * t

Substitute symbolic abstract locations and symbolic interval value in the array block. eval_sym is to get substituted interval values and eval_locpath is to get substituted abstract locaion values. It also returns a set of abstract locations containing non-allocsite locations from the substitution results. Since the key of ArrayBlk.t is AbsLoc.Allocsite.t, they cannot be written in this domain.

val set_length : Itv.t -> t -> t
val set_offset : Itv.t -> t -> t
val set_stride : Z.t -> t -> t
val get_symbols : t -> BO.Symb.SymbolSet.t

Return all symbols for integer values in it

val get_offset : ?⁠cost_mode:bool -> t -> Itv.t

Return offset of the array block. If cost_mode is true, it returns a conservative (bigger than correct one), but not correct offset results.

val get_size : ?⁠cost_mode:bool -> t -> Itv.t

Return size of the array block. If cost_mode is true, it returns a conservative (bigger than correct one), but not correct size results.