Module Pulselib.PulseBaseDomain

module F = Stdlib.Format
type t = {
heap : PulseBaseMemory.t;
stack : PulseBaseStack.t;
attrs : PulseBaseAddressAttributes.t;
}
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
type cell = PulseBaseMemory.Edges.t * PulseBasicInterface.Attributes.t
val empty : t
val reachable_addresses : t -> Pulselib.PulseBasicInterface.AbstractValue.Set.t

compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from the stack variables

val reachable_addresses_from : PulseBasicInterface.AbstractValue.t list -> t -> Pulselib.PulseBasicInterface.AbstractValue.Set.t

compute the set of abstract addresses that are reachable from given abstract addresses

type mapping
val empty_mapping : mapping
type isograph_relation =
| NotIsomorphic

no mapping was found that can make LHS the same as the RHS

| IsomorphicUpTo of mapping

mapping(lhs) is isomorphic to rhs

val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
val is_isograph : lhs:t -> rhs:t -> mapping -> bool
val find_cell_opt : PulseBasicInterface.AbstractValue.t -> t -> cell option
val pp : F.formatter -> t -> unit
val subst_var : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.AbstractValue.t) -> t -> t PulseBasicInterface.SatUnsat.t