PulseSummary (infer.Pulselib.PulseSummary)

type pre_post_list = Pulselib.PulseDomainInterface.ExecutionDomain.summary list

val yojson_of_pre_post_list : 
  pre_post_list ->
  Ppx_yojson_conv_lib.Yojson.Safe.t

type summary = {

pre_post_list : pre_post_list;
non_disj : Pulselib.PulseDomainInterface.NonDisjDomain.Summary.t;

}

val yojson_of_summary : summary -> Ppx_yojson_conv_lib.Yojson.Safe.t

type t = {

main : summary;
specialized : summary IR.Specialization.Pulse.Map.t;

}

val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t

val of_posts : 
  t Absint.InterproceduralAnalysis.t ->
  IR.Specialization.Pulse.t option ->
  IBase.Location.t ->
  (Pulselib.PulseDomainInterface.ExecutionDomain.t
   * Pulselib.PulseDomainInterface.PathContext.t)
    list ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  summary

val add_disjunctive_pre_post : 
  Pulselib.PulseDomainInterface.ExecutionDomain.summary ->
  summary ->
  summary

val empty : summary

val join : summary -> summary -> summary

val force_exit_program : 
  t Absint.InterproceduralAnalysis.t ->
  Pulselib.PulseDomainInterface.PathContext.t ->
  IBase.Location.t ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t ->
  _ Pulselib.PulseDomainInterface.ExecutionDomain.base_t
    Pulselib.PulseBasicInterface.SatUnsat.t

val pp : 
  IStdlib.Pp.env ->
  IR.Procname.t ->
  Stdlib.Format.formatter ->
  t ->
  unit

val append_objc_actual_self_positive : 
  IR.Procname.t ->
  IR.ProcAttributes.t ->
  ((Pulselib.PulseBasicInterface.AbstractValue.t
    * Pulselib.PulseBasicInterface.ValueHistory.t)
   * IR.Typ.t)
    option ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t
    Pulselib.PulseDomainInterface.AccessResult.t
    Pulselib.PulseBasicInterface.SatUnsat.t

val initial_with_positive_self : 
  IR.ProcAttributes.t ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t

The initial state of the analysis, with the additional path condition self > 0 for Objective-C and this>0 for C++ instance methods.

val mk_objc_nil_messaging_summary : 
  IR.Tenv.t ->
  IR.ProcAttributes.t ->
  Pulselib.PulseDomainInterface.ExecutionDomain.summary option

val merge : t -> t -> t

Merge specialized summaries.