Module InferModules.JavaTrace

include Trace.S
include Trace.Spec
module Source : Source.S
module Sink : Sink.S
val get_report : Source.t ‑> Sink.t ‑> Sanitizer.t list ‑> InferBase.IssueType.t option

return Some(issue) a trace from source to sink passing through the given sanitizers should be reported, None otherwise

type t
type astate = t
include AbstractDomain.WithBottom with type astate := astate
include AbstractDomain.S
type astate
val (<=) : lhs:astate ‑> rhs:astate ‑> bool

the partial order induced by join

val join : astate ‑> astate ‑> astate
val widen : prev:astate ‑> next:astate ‑> num_iters:int ‑> astate
val pp : InferModules.AbstractDomain.F.formatter ‑> astate ‑> unit
val empty : astate

The bottom value of the domain. Naming it empty instead of bottom helps to bind the empty value for sets and maps to the natural definition for bottom

val is_empty : astate ‑> bool

Return true if this is the bottom value

module Sources : sig ... end
module Sinks = Sink.Set
module Passthroughs = Passthrough.Set
type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list

path from a source to a sink with passthroughs at each step in the call stack. the first set of passthroughs are the ones in the "reporting" procedure that calls the first function in both the source and sink stack

type report = {
issue : InferBase.IssueType.t;
path_source : Source.t;
path_sink : Sink.t;
path_passthroughs : Passthroughs.t;
}
val empty : t

the empty trace

val sources : t ‑> Sources.t

get the sources of the trace.

val sinks : t ‑> Sinks.t

get the sinks of the trace

val passthroughs : t ‑> Passthroughs.t

get the passthroughs of the trace

val get_reports : ?⁠cur_site:InferIR.CallSite.t ‑> t ‑> report list

get the reportable source-sink flows in this trace. specifying cur_site restricts the reported paths to ones introduced by the call at cur_site

val get_reportable_paths : ?⁠cur_site:InferIR.CallSite.t ‑> t ‑> trace_of_pname:(InferIR.Typ.Procname.t ‑> t) ‑> path list

get a path for each of the reportable source -> sink flows in this trace. specifying cur_site restricts the reported paths to ones introduced by the call at cur_site

val to_loc_trace : ?⁠desc_of_source:(Source.t ‑> string) ‑> ?⁠source_should_nest:(Source.t ‑> bool) ‑> ?⁠desc_of_sink:(Sink.t ‑> string) ‑> ?⁠sink_should_nest:(Sink.t ‑> bool) ‑> path ‑> InferIR.Errlog.loc_trace

create a loc_trace from a path; source_should_nest s should be true when we are going one deeper into a call-chain, ie when lt_level should be bumper in the next loc_trace_elem, and similarly for sink_should_nest

val of_source : Source.t ‑> t

create a trace from a source

val of_footprint : InferIR.AccessPath.Abs.t ‑> t

create a trace from a footprint access path

val add_source : Source.t ‑> t ‑> t

add a source to the current trace

val add_sink : Sink.t ‑> t ‑> t

add a sink to the current trace.

val add_sanitizer : Sanitizer.t ‑> t ‑> t

add a sanitizer to the current trace

val update_sources : t ‑> Sources.t ‑> t
val update_sinks : t ‑> Sinks.t ‑> t

replace sinks with new ones

val get_footprint_indexes : t ‑> InferStdlib.IntSet.t

get the footprint indexes for all of the sources in the trace

val append : t ‑> t ‑> InferIR.CallSite.t ‑> t

append the trace for given call site to the current caller trace

val is_empty : t ‑> bool

return true if this trace has no source or sink data

val pp : InferModules.Trace.F.formatter ‑> t ‑> unit
val pp_path : InferIR.Typ.Procname.t ‑> InferModules.Trace.F.formatter ‑> path ‑> unit

pretty-print a path in the context of the given procname