Module BO__AbsLoc.PowLoc

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 compare : t -> t -> int
val get_parent_field : t -> t
val append_field : ?⁠typ:IR.Typ.t -> t -> fn:IR.Fieldname.t -> t
val append_star_field : t -> fn:IR.Fieldname.t -> t
val bot : t
val add : Loc.t -> t -> t
val of_list : Loc.t list -> t
val exists : (Loc.t -> bool) -> t -> bool
val mem : Loc.t -> t -> bool
val is_singleton_or_more : t -> Loc.t IStdlib.IContainer.singleton_or_more
val min_elt_opt : t -> Loc.t option
val singleton : Loc.t -> t
val fold : (Loc.t -> 'a -> 'a) -> t -> 'a -> 'a
val cast : IR.Typ.t -> t -> t
val of_c_strlen : t -> t

It appends the strlen field.

val unknown : t
val exists_str : f:(string -> bool) -> t -> bool

It checks if a variable or a field name in the location path satisfies f.

val is_bot : t -> bool
type eval_locpath = BO.Symb.SymbolPath.partial -> t

Type for evaluating a path to an abstract location.

val subst : t -> eval_locpath -> t

It substitutes paths in the abstract location using eval_locpath.

val subst_loc : Loc.t -> eval_locpath -> t

It substitutes paths in the abstract location using eval_locpath.

val lift_cmp : BO.Boolean.EqualOrder.t -> t -> t -> BO.Boolean.t

It lifts a comparison of Loc.t to t. The comparison can be Boolean.EqualOrder.eq, Boolean.EqualOrder.ne, etc.

val to_set : t -> LocSet.t
val get_linked_list_next : lhs:t -> rhs:t -> Loc.t option

It checks whether rhs is of lhs.any_field, which is a heuristic for detecting a linked list, e.g. x = x.next(). It returns Some lhs if the condition is satisfied, None otherwise.