Mt_shared_vars.Precise
include Computer
with module Access = Mt_cfg_types.NodeIdAccess
and module Set = Mt_cfg_types.SetNodeIdAccess
module Access = Mt_cfg_types.NodeIdAccess
module Set = Mt_cfg_types.SetNodeIdAccess
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
val enumerate_written_vars_value :
ZoneMap.map ->
(Eva__.Thread.t * Frama_c_kernel.Base.t * Frama_c_kernel.Cvalue.V_Offsetmap.t)
list
val remove_non_concur_zones_from_cfg :
Frama_c_kernel.Locations.Zone.t ->
Mt_cfg_types.CfgNode.t ->
unit
val mark_concur_access_in_cfg : ('a * Set.t) list -> unit