Mthread.Mt_mutexes
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
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 need_sync :
'a Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t ->
(Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.key * 'a) list