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 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 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_recursive_calls : summary -> PulseMutualRecursion.Set.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