Frama-C:
Plug-ins:
Libraries:

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 clear_non_globals : Types.state -> Types.state

Remove all the values that are not global variables from the 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.

Conversion to and from Mthread world to the value analysis

type 'a conversion = ('a, string) Frama_c_kernel.Result.t
val extract_pointer : Types.value -> Types.pointer conversion
val extract_int : Types.value -> int conversion
val extract_int_possibly_zero : Types.value -> (int * [ `Exact | `WithZero ]) conversion
val extract_constant_string : Types.value -> string conversion
val extract_int_list : cardinal:int -> Types.value -> int list conversion

Fails if value represents more than cardinal integers.

val int_to_value : int -> Types.value