Frama-C API - `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 display_shared_vars_value : ZoneMap.map -> unit

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

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

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

Frama-C API - Precise