package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `Mt_shared_vars.Precise`Source

include Computer
  with module Access = Mt_cfg_types.NodeIdAccess
   and module Set = Mt_cfg_types.SetNodeIdAccess

Sourcemodule Access = Mt_cfg_types.NodeIdAccess

Sourcemodule Set = Mt_cfg_types.SetNodeIdAccess

Source

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

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

Source

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

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

Source

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

Sourceval display_shared_vars_value : ZoneMap.map -> unit

Source

val enumerate_written_vars_value : 
  ZoneMap.map ->
  (Eva__.Thread.t * Frama_c_kernel.Base.t * Frama_c_kernel.Cvalue.V_Offsetmap.t)
    list

Source

val join_shared_values : 
  ('a * Frama_c_kernel.Base.t * Frama_c_kernel.Cvalue.Model.offsetmap) list ->
  Frama_c_kernel.Cvalue.Model.t

Source

val remove_non_concur_zones_from_cfg : 
  Frama_c_kernel.Locations.Zone.t ->
  Mt_cfg_types.CfgNode.t ->
  unit

Sourceval mark_concur_access_in_cfg : ('a * Set.t) list -> unit

package frama-c

Module Mt_shared_vars.PreciseSource

Module `Mt_shared_vars.Precise`Source