Types (frama-c-eva.Mthread.Mt

type pointer = Frama_c_kernel.Cil_types.varinfo * int

Pointers are the address of a variable, with a potential offset, and are used to refer in a simple way to an address 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

type state_accesser =

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