MutexAnalysisData race analysis.
module M = Messagesmodule GU = Goblintutilmodule Addr = ValueDomain.Addrmodule Offs = ValueDomain.Offsmodule Lockset = LockDomain.Locksetmodule Mutexes = LockDomain.Mutexesmodule AD = ValueDomain.ADmodule ID = ValueDomain.IDmodule IdxDom = ValueDomain.IndexDomainmodule LockingPattern = Exp.LockingPatternmodule Exp = Exp.Expmodule LF = LibraryFunctionsval big_kernel_lock : LockDomain.Addr.tval console_sem : LockDomain.Addr.tval verifier_atomic : LockDomain.Addr.tmodule type SpecParam = sig ... endData race analyzer without base --- this is the new standard
module MyParam : sig ... endmodule WriteBased : sig ... endmodule Spec : sig ... end