Mthread.Mt_mutexes_typestype mutexes_by_access = {mutexes_for_read : access_or_protection;mutexes_for_write : access_or_protection;}module MutexesByAccess : sig ... endmodule LatticeMutexes :
Frama_c_kernel.Lmap_bitwise.With_default with type t = mutexes_by_accessmodule MutexesByZone :
Frama_c_kernel.Lmap_bitwise.Location_map_bitwise
with type v = mutexes_by_access