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 {
  1. elem : elem_t;
  2. loc : IBase.Location.t;
  3. 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 t := t
include IStdlib.PrettyPrintable.PrintableOrderedType with type t := t
include Stdlib.Set.OrderedType with type t := t
val compare : t -> t -> int
include IStdlib.PrettyPrintable.PrintableType with type t := 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 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.

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