Mt_memory.Types
type pointer = Frama_c_kernel.Cil_types.varinfo * int
Pointers are the adress of a variable, with a potential offset, and are used to refer in a simple way to an adress in memory
module Pointer :
Frama_c_kernel.Datatype.S_with_collections with type t = pointer
type state = Frama_c_kernel.Cvalue.Model.t
type value = Frama_c_kernel.Cvalue.V.t
type zone = Frama_c_kernel.Locations.Zone.t
type slice = Frama_c_kernel.Cvalue.V_Offsetmap.t
type functions_states = state Frama_c_kernel.Cil_datatype.Stmt.Hashtbl.t
type map_functions_states = state Frama_c_kernel.Cil_datatype.Stmt.Map.t
val map_functions_states_to_get_state :
map_functions_states ->
Frama_c_kernel.Cil_types.stmt ->
state
val iter_requests :
state_accesser ->
Frama_c_kernel.Cil_types.stmt ->
(Eva.Results.request -> unit) ->
unit
val merge_map_non_map_functions_states :
map_functions_states ->
functions_states ->
map_functions_states
val merge_map_functions_states :
map_functions_states ->
map_functions_states ->
map_functions_states