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 check_valid : PulseBasicInterface.Trace.t -> PulseBasicInterface.AbstractValue.t -> t -> (tPulseBasicInterface.Invalidation.t * PulseBasicInterface.Trace.t) IStdlib.IStd.result
val invalidate : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> PulseBasicInterface.Invalidation.t -> IBase.Location.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.Name.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