Module `Mthread.Mt_mutexes`Source

Source

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

Source

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

Sourcetype protection =

| Unprotected
| Priority
| Protected of Eva__.Mutex.Set.t

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mthread/Mthread/Mt_mutexes/index.html

Module `Mthread.Mt_mutexes`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mthread/Mthread/Mt_mutexes/index.html

Module Mthread.Mt_mutexesSource

Module `Mthread.Mt_mutexes`Source