Mt_mutexes (frama-c-eva.Mthread.Mt

val mutexes_protecting_zones' : 
  (Frama_c_kernel.Locations.Zone.t * Mt_cfg_types.SetNodeIdAccess.t) list ->
  Mt_mutexes_types.MutexesByZone.t

val pretty_with_mutexes : 
  Stdlib.Format.formatter ->
  Mt_shared_vars.Precise.list_accesses ->
  unit

type protection =

| Unprotected
| Priority

val pretty_protection : Stdlib.Format.formatter -> protection -> unit

val pretty_protection_per_thread : 
  Stdlib.Format.formatter ->
  (Mt_thread.thread * Mt_thread.thread * protection) ->
  unit

type zone_protection =
  (Frama_c_kernel.Locations.Zone.t
   * (Mt_thread.thread * Mt_thread.thread * protection) list)
    list

val pretty_zone_protection : 
  Stdlib.Format.formatter ->
  (Frama_c_kernel.Locations.Zone.t
   * (Mt_thread.thread * Mt_thread.thread * protection) list) ->
  unit

val check_protection : 
  Mt_thread.analysis_state ->
  Mt_shared_vars.Precise.list_accesses ->
  zone_protection

val pretty_protections : 
  Stdlib.Format.formatter ->
  (Frama_c_kernel.Locations.Zone.t
   * (Mt_thread.thread * Mt_thread.thread * protection) list)
    list ->
  unit

val ill_protected : 
  Mt_shared_vars.Precise.list_accesses ->
  zone_protection ->
  Frama_c_kernel.Locations.Zone.t Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t

val need_sync : 
  'a Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t ->
  (Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.key * 'a) list