Summary (infer.Pulselib.PulseAbductiveDomain.Summary)

type summary = private t

private type to make sure of_post is always called when creating summaries and that it is not called twice

val compare_summary : summary -> summary -> int

val equal_summary : summary -> summary -> bool

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

val add_need_dynamic_type_specialization : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  summary ->
  summary

val of_post : 
  IR.Procname.t ->
  IR.ProcAttributes.t ->
  IBase.Location.t ->
  t ->
  (summary,
    [> `JavaResourceLeak of
         summary
         * t
         * IR.JavaClassName.t
         * Pulselib.PulseBasicInterface.Trace.t
         * IBase.Location.t
    | `HackUnawaitedAwaitable of
      summary * t * Pulselib.PulseBasicInterface.Trace.t * IBase.Location.t
    | `CSharpResourceLeak of
      summary
      * t
      * IR.CSharpClassName.t
      * Pulselib.PulseBasicInterface.Trace.t
      * IBase.Location.t
    | `MemoryLeak of
      summary
      * t
      * Pulselib.PulseBasicInterface.Attribute.allocator
      * Pulselib.PulseBasicInterface.Trace.t
      * IBase.Location.t
    | `PotentialInvalidAccessSummary of
      summary
      * t
      * DecompilerExpr.t
      * (Pulselib.PulseBasicInterface.Trace.t
         * Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
             option) ])
    IStdlib.IStd.result
    Pulselib.PulseBasicInterface.SatUnsat.t

Trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state.

val leq : lhs:summary -> rhs:summary -> bool

val pp : F.formatter -> summary -> unit

val get_pre : summary -> BaseDomain.t

val get_post : summary -> BaseDomain.t

val get_path_condition : summary -> Pulselib.PulseBasicInterface.Formula.t

val get_topl : summary -> PulseTopl.state

val heap_paths_that_need_dynamic_type_specialization : 
  summary ->
  Pulselib.PulseBasicInterface.AbstractValue.t IR.Specialization.HeapPath.Map.t

val get_skipped_calls : summary -> Pulselib.PulseBasicInterface.SkippedCalls.t

val is_heap_allocated : 
  summary ->
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  bool

whether the abstract value provided has edges in the pre or post heap

val get_must_be_valid : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  summary ->
  (Pulselib.PulseBasicInterface.Timestamp.t
   * Pulselib.PulseBasicInterface.Trace.t
   * Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option)
    option

val remove_all_must_not_be_tainted : 
  ?kinds:Pulselib.PulseBasicInterface.TaintConfig.Kind.Set.t ->
  summary ->
  summary

val pre_heap_has_assumptions : summary -> bool

whether the pre heap encodes some assumptions about values: either a value is restricted (>= 0) or there is sharing in the heap. Both represent implicit assumptions that the program must have made.

type t = summary

include Ppx_compare_lib.Comparable.S with type t := t

val compare : t Base__Ppx_compare_lib.compare

include Ppx_compare_lib.Equal.S with type t := t

val equal : t Base__Ppx_compare_lib.equal

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

val get_transitive_info : t -> Pulselib.PulseBasicInterface.TransitiveInfo.t