Computer (frama-c-eva.Mthread.Mt_shared

module Access : Frama_c_kernel.Datatype.S

module Set : Frama_c_kernel.Lattice_type.Lattice_Set with type O.elt = Access.t

module ZoneMap : 
  Frama_c_kernel.Lmap_bitwise.Location_map_bitwise with type v = Set.t

type list_accesses = (Frama_c_kernel.Locations.Zone.t * Set.t) list

val pretty_concurrent_accesses : 
  ?f:Access.t Frama_c_kernel.Pretty_utils.formatter ->
  unit ->
  Stdlib.Format.formatter ->
  list_accesses ->
  unit

val all_zones_accessed : list_accesses -> Frama_c_kernel.Locations.Zone.t

val concurrent_accesses_all_threads : 
  Mt_thread.ThreadState.t list ->
  (list_accesses * list_accesses) * ZoneMap.map