Module InferModules.RacerDDomain

module F = Format

module Access : sig ... end

module TraceElem : sig ... end

module PathDomain : SinkTrace.S with module Source = Source.Dummy and module Sink = SinkTrace.MakeSink(TraceElem)

module LocksDomain : sig ... end

Overapproximation of number of locks that are currently held

module ThreadsDomain : sig ... end

Abstraction of threads that may run in parallel with the current thread. NoThread < AnyThreadExceptSelf < AnyThread

module AccessSnapshot : sig ... end

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

module AccessDomain : module type of sig ... end

map of access metadata |-> set of accesses. the map should hold all accesses to a possibly-unowned access path

module OwnershipAbstractValue : sig ... end

Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) and top element (Unowned)

module OwnershipDomain : sig ... end

module Choice : sig ... end

attribute attached to a boolean variable specifying what it means when the boolean is true

module Attribute : sig ... end

module AttributeSetDomain : module type of sig ... end

module AttributeMapDomain : sig ... end

module StabilityDomain : sig ... end

type astate = {

`threads : ThreadsDomain.astate;`	(** current thread: main, background, or unknown *)
`locks : LocksDomain.astate;`	(** boolean that is true if a lock must currently be held *)
`accesses : AccessDomain.astate;`	(** read and writes accesses performed without ownership permissions *)
`ownership : OwnershipDomain.astate;`	(** map of access paths to ownership predicates *)
`attribute_map : AttributeMapDomain.astate;`	(** map of access paths to attributes such as owned, functional, ... *)
`wobbly_paths : StabilityDomain.astate;`	(** Record the "touched" paths that can compromise the race detection * *)

}

type summary = {

threads : ThreadsDomain.astate;

locks : LocksDomain.astate;

accesses : AccessDomain.astate;

return_ownership : OwnershipAbstractValue.astate;

return_attributes : AttributeSetDomain.astate;

wobbly_paths : StabilityDomain.astate;

}

same as astate, but without attribute_map (since these involve locals) and with the addition of the ownership/attributes associated with the return value as well as the set of formals which may escape

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

val pp_summary : F.formatter ‑> summary ‑> unit