Module Pulselib__PulseAbductiveDomain.AddressAttributes
attribute operations like BaseAddressAttributes
but that also take care of propagating facts to the precondition
val abduce_and_add : Pulselib.PulseBasicInterface.AbstractValue.t -> Pulselib.PulseBasicInterface.Attributes.t -> t -> t
add the attributes to both the current state and, if meaningful, the pre
val add_one : Pulselib.PulseBasicInterface.AbstractValue.t -> Pulselib.PulseBasicInterface.Attribute.t -> t -> t
add the attribute only to the post
val check_valid : Pulselib.PulseBasicInterface.Trace.t -> Pulselib.PulseBasicInterface.AbstractValue.t -> t -> (t, Pulselib.PulseBasicInterface.Invalidation.t * Pulselib.PulseBasicInterface.Trace.t) IStdlib.IStd.result
val invalidate : (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> Pulselib.PulseBasicInterface.Invalidation.t -> IBase.Location.t -> t -> t
val allocate : IR.Procname.t -> (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> IBase.Location.t -> t -> t
val add_dynamic_type : IR.Typ.Name.t -> Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val remove_allocation_attr : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val get_closure_proc_name : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> IR.Procname.t option
val is_end_of_collection : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> bool
val mark_as_end_of_collection : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val is_std_vector_reserved : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> bool
val std_vector_reserve : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val find_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> Pulselib.PulseBasicInterface.Attributes.t option