package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Mt_shared_vars.PreciseSource

include Computer with module Access = Mt_cfg_types.NodeIdAccess and module Set = Mt_cfg_types.SetNodeIdAccess
Sourcetype list_accesses = (Frama_c_kernel.Locations.Zone.t * Set.t) list
Sourceval pretty_concurrent_accesses : ?f:Access.t Frama_c_kernel.Pretty_utils.formatter -> unit -> Stdlib.Format.formatter -> list_accesses -> unit
Sourceval concurrent_accesses_all_threads : Mt_thread.ThreadState.t list -> (list_accesses * list_accesses) * ZoneMap.map
Sourceval display_shared_vars_value : ZoneMap.map -> unit
Sourceval enumerate_written_vars_value : ZoneMap.map -> (Eva__.Thread.t * Frama_c_kernel.Base.t * Frama_c_kernel.Cvalue.V_Offsetmap.t) list
Sourceval 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
OCaml

Innovation. Community. Security.