Module `PulseAbductiveDomain.AddressAttributes`

attribute operations like BaseAddressAttributes but that also take care of propagating facts to the precondition

val abduce_and_add : PulseBasicInterface.AbstractValue.t -> PulseBasicInterface.Attributes.t -> t -> t: add the attributes to both the current state and, if meaningful, the pre

val add_one : PulseBasicInterface.AbstractValue.t -> PulseBasicInterface.Attribute.t -> t -> t: add the attribute only to the post

val add_attrs : PulseBasicInterface.AbstractValue.t -> PulseBasicInterface.Attributes.t -> t -> t
val check_valid : PulseBasicInterface.Trace.t -> PulseBasicInterface.AbstractValue.t -> t -> (t, PulseBasicInterface.Invalidation.t * PulseBasicInterface.Trace.t) IStdlib.IStd.result
val check_initialized : PulseBasicInterface.Trace.t -> PulseBasicInterface.AbstractValue.t -> t -> (t, unit) IStdlib.IStd.result
val invalidate : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> PulseBasicInterface.Invalidation.t -> IBase.Location.t -> t -> t
val replace_must_be_valid_reason : PulseBasicInterface.Invalidation.must_be_valid_reason -> PulseBasicInterface.AbstractValue.t -> t -> t
val allocate : IR.Procname.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> IBase.Location.t -> t -> t
val add_dynamic_type : IR.Typ.t -> PulseBasicInterface.AbstractValue.t -> t -> t
val remove_allocation_attr : PulseBasicInterface.AbstractValue.t -> t -> t
val get_closure_proc_name : PulseBasicInterface.AbstractValue.t -> t -> IR.Procname.t option
val is_end_of_collection : PulseBasicInterface.AbstractValue.t -> t -> bool
val mark_as_end_of_collection : PulseBasicInterface.AbstractValue.t -> t -> t
val is_std_vector_reserved : PulseBasicInterface.AbstractValue.t -> t -> bool
val std_vector_reserve : PulseBasicInterface.AbstractValue.t -> t -> t
val find_opt : PulseBasicInterface.AbstractValue.t -> t -> PulseBasicInterface.Attributes.t option
val check_valid_isl : PulseBasicInterface.Trace.t -> PulseBasicInterface.AbstractValue.t -> ?⁠null_noop:bool -> t -> (t, [> `ISLError of t | `InvalidAccess of PulseBasicInterface.Invalidation.t * PulseBasicInterface.Trace.t * t ]) IStdlib.IStd.result list