Frama-C API - Mt_memory
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