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 -> tadd the attributes to both the current state and, if meaningful, the pre
val add_one : Pulselib.PulseBasicInterface.AbstractValue.t -> Pulselib.PulseBasicInterface.Attribute.t -> t -> tadd 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.resultval invalidate : (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> Pulselib.PulseBasicInterface.Invalidation.t -> IBase.Location.t -> t -> tval allocate : IR.Procname.t -> (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> IBase.Location.t -> t -> tval add_dynamic_type : IR.Typ.Name.t -> Pulselib.PulseBasicInterface.AbstractValue.t -> t -> tval remove_allocation_attr : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> tval get_closure_proc_name : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> IR.Procname.t optionval is_end_of_collection : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> boolval mark_as_end_of_collection : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> tval is_std_vector_reserved : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> boolval std_vector_reserve : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> tval find_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> Pulselib.PulseBasicInterface.Attributes.t option