Module Mthread.Mt_memorySource

Sourcemodule Types : sig ... end

Union of state, values and list of values

Sourceval 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!

Sourceval join_value : Types.value -> Types.value -> Types.value * bool
Sourceval join_params : Types.value list -> Types.value list -> Types.value list * bool
Sourceval clear_non_globals : Types.state -> Types.state

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

Reading and writing in memory

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

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

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

Return the value pointed by the given int pointer

Sourceval 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.

Sourceval 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.

Sourceval 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

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

Fails if value represents more than cardinal integers.

Sourceval int_to_value : int -> Types.value