Module 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_topl : summary -> PulseTopl.state
val heap_paths_that_need_dynamic_type_specialization : summary -> Pulselib.PulseBasicInterface.AbstractValue.t IR.Specialization.HeapPath.Map.t
val get_recursive_calls : summary -> PulseMutualRecursion.Set.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 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