Module Concurrency.RacerDDomain

module AccessExpression = Absint.HilExp.AccessExpression
module F = Stdlib.Format
val apply_to_first_actual : Absint.HilExp.t list -> 'a -> f:(Absint.HilExp.access_expression -> 'a) -> 'a
val pp_exp : F.formatter -> AccessExpression.t -> unit

language sensitive pretty-printer

module Access : sig ... end
module LockDomain : sig ... end

Overapproximation of number of times the lock has been acquired

module ThreadsDomain : sig ... end

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

module OwnershipAbstractValue : sig ... end
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 OwnershipDomain : sig ... end
module Attribute : sig ... end
module AttributeMapDomain : sig ... end
type t = {
  1. threads : ThreadsDomain.t;
    (*

    current thread: main, background, or unknown

    *)
  2. locks : LockDomain.t;
    (*

    boolean that is true if a lock must currently be held

    *)
  3. never_returns : NeverReturns.t;
    (*

    boolean which is true if a noreturn call is always reached

    *)
  4. accesses : AccessDomain.t;
    (*

    read and writes accesses performed without ownership permissions

    *)
  5. ownership : OwnershipDomain.t;
    (*

    map of access paths to ownership predicates

    *)
  6. attribute_map : AttributeMapDomain.t;
    (*

    map of access paths to attributes such as owned, functional, ...

    *)
}
include Absint.AbstractDomain.S with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val initial : t
val add_unannotated_call_access : Absint.FormalMap.t -> IR.Procname.t -> Absint.HilExp.t list -> IBase.Location.t -> t -> t
type summary = {
  1. threads : ThreadsDomain.t;
  2. locks : LockDomain.t;
  3. never_returns : NeverReturns.t;
  4. accesses : AccessDomain.t;
  5. return_ownership : OwnershipAbstractValue.t;
  6. return_attribute : Attribute.t;
  7. attributes : AttributeMapDomain.t;
}

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

val empty_summary : summary
val pp_summary : F.formatter -> summary -> unit
val astate_to_summary : IR.Procdesc.t -> Absint.FormalMap.t -> t -> summary
val add_access : IR.Tenv.t -> Absint.FormalMap.t -> IBase.Location.t -> is_write:bool -> t -> Absint.HilExp.t -> t
val add_container_access : IR.Tenv.t -> Absint.FormalMap.t -> is_write:bool -> Absint.AccessPath.base -> IR.Procname.t -> Absint.HilExp.t list -> IBase.Location.t -> t -> t
val add_reads_of_hilexps : IR.Tenv.t -> Absint.FormalMap.t -> Absint.HilExp.t list -> IBase.Location.t -> t -> t
val acquire_lock : t -> t
val release_lock : t -> t
val lock_if_true : Absint.HilExp.access_expression -> t -> t
val branch_never_returns : unit -> t