AbsLoc.PowLoc
include Absint.AbstractDomain.S
include Absint.AbstractDomain.Comparable
include IStdlib.PrettyPrintable.PrintableType
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
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 is_singleton_or_more : t -> Loc.t IStdlib.IContainer.singleton_or_more
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 = 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 : Boolean.EqualOrder.t -> t -> t -> Boolean.t
It lifts a comparison of Loc.t
to t
. The comparison can be Boolean.EqualOrder.eq
, Boolean.EqualOrder.ne
, etc.
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.
val is_unknown : t -> bool
val is_single_known_loc : t -> bool
Returns true if the set consists of a single known location.