Module Goblint_lib.CommonPriv

Thread-modular value analysis utilities for BasePriv and RelationPriv.

module Q = Queries
module IdxDom = ValueDomain.IndexDomain
module type AtomicParam = sig ... end
module ConfCheck : sig ... end
module Protection : sig ... end
module MutexGlobals : sig ... end
module MayVars : sig ... end
module MustVars : sig ... end
module Locksets : sig ... end
module WriteCenteredD : sig ... end
module type Digest = sig ... end

Digest to be used for analyses that account for all join-local contributions in some locally tracked datastructure, akin to the L component from the analyses in

Ego-Lane Derived digest based on whether given threads have been started yet, can be used to refine any analysis @see PhD thesis of M. Schwarz once it is published ;)

module PerMutexTidCommon (Digest : Digest) (LD : Lattice.S) : sig ... end