Module RacerDDomain.AccessSnapshot

snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held, ownership precondition

module AccessSnapshotElem : sig ... end
include Absint.ExplicitTrace.TraceElem with type elem_t = AccessSnapshotElem.t
type elem_t = AccessSnapshotElem.t
type t = private {
elem : elem_t;
loc : IBase.Location.t;
trace : Absint.CallSite.t list;
}

An elem which occured at loc, after the chain of steps (usually calls) in trace.

Both pp and describe simply call the same function on the trace element.

include Absint.ExplicitTrace.Element with type Element.t := t
include IStdlib.PrettyPrintable.PrintableOrderedType
include IStdlib.IStd.Caml.Set.OrderedType
type t
val compare : t -> t -> int
include IStdlib.PrettyPrintable.PrintableType with type t := t
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val describe : Stdlib.Format.formatter -> t -> unit

Pretty printer used for trace construction; pp is used for debug output.

val make : elem_t -> IBase.Location.t -> t
val map : f:(elem_t -> elem_t) -> t -> t
val get_loc : t -> IBase.Location.t

Starting location of the trace: this is either loc if trace==[], or the head of trace.

val make_loc_trace : ?⁠nesting:int -> t -> Absint.Errlog.loc_trace
val with_callsite : t -> Absint.CallSite.t -> t

Push given callsite onto trace, extending the call chain by one.

module FiniteSet : Absint.ExplicitTrace.FiniteSet with type FiniteSet.elt = t

A powerset of traces.

val is_write : t -> bool

is it a write OR a container write

val is_container_write : t -> bool
val get_loc : t -> IBase.Location.t
val is_unprotected : t -> bool

return true if not protected by lock, thread, or ownership