Mt_memory (frama-c-eva.Mthread.Mt

module Types : sig ... end

Union of state, values and list of values

val join_state : Types.state -> Types.state -> Types.state * bool

. We also return a boolean indicating whether an update has taken place, ie. if the result of the union is different (thus greater) from the first argument. Notice that this means that those functions are not symmetrical!

val join_value : Types.value -> Types.value -> Types.value * bool

val join_params : 
  Types.value list ->
  Types.value list ->
  Types.value list * bool

val join_zone : Types.zone -> Types.zone -> Types.zone * bool

val clear_non_globals : Types.state -> Types.state

Remove all the values that are not global variables from the state

val is_frama_c_var : Frama_c_kernel.Cil_types.varinfo -> bool

Functions dealing with frama-c special variables

val is_frama_c_base : Frama_c_kernel.Base.t -> bool

val remove_frama_c_var_from_zone : Types.zone -> Types.zone

val remove_frama_c_var_from_mem : Types.state -> Types.state

Reading and writing in memory

val read_slice : p:Types.value -> sbytes:int -> Types.state -> Types.slice

read_slice ~p ~sbytes st reads sbytes starting from p in state.

val read_int_pointer : Types.pointer -> Types.state -> Types.value

Return the value pointed by the given int pointer

val write_int_pointer : Types.pointer -> int -> Types.state -> Types.state

write_int_pointer p v state write the int v at the location pointed p in state state.

val replace_value_at_int_pointer : 
  Types.pointer ->
  before:int ->
  after:int ->
  Types.state ->
  Types.state

replace_value_at_int_pointer p ~before ~after state replaces before by after in the abstract value bound at location p in state.

val write_slice : 
  p:Types.pointer ->
  sbytes:int ->
  slice:Types.slice ->
  exact:bool ->
  Types.state ->
  Types.state

write_at_pointer ~p ~sbytes ~slice st alters state by writing at the sbytes bytes starting at p the slice v.

val lval_from_pointer : Types.pointer -> Frama_c_kernel.Cil_types.lval

Conversion to and from Mthread world to the value analysis

val extract_fun : 
  Types.value ->
  Frama_c_kernel.Cil_types.kernel_function Mt_lib.conversion

val extract_pointer : Types.value -> Types.pointer Mt_lib.conversion

val extract_int : Types.value -> int Mt_lib.conversion

val extract_int_possibly_zero : 
  Types.value ->
  (int * [ `Exact | `WithZero ]) Mt_lib.conversion

val extract_constant_string : Types.value -> string Mt_lib.conversion

val extract_non_wide_string : 
  Frama_c_kernel.Base.cstring ->
  string Mt_lib.conversion

val int_to_value : int -> Types.value

val pretty_slice : Types.slice Frama_c_kernel.Pretty_utils.formatter