package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 join_zone : Types.zone -> Types.zone -> Types.zone * bool
Sourceval clear_non_globals : Types.state -> Types.state

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

Sourceval is_frama_c_var : Frama_c_kernel.Cil_types.varinfo -> bool

Functions dealing with frama-c special variables

Sourceval is_frama_c_base : Frama_c_kernel.Base.t -> bool
Sourceval remove_frama_c_var_from_zone : Types.zone -> Types.zone
Sourceval remove_frama_c_var_from_mem : Types.state -> Types.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

Sourceval extract_int : Types.value -> int Mt_lib.conversion
Sourceval extract_int_possibly_zero : Types.value -> (int * [ `Exact | `WithZero ]) Mt_lib.conversion
Sourceval extract_constant_string : Types.value -> string Mt_lib.conversion
Sourceval extract_non_wide_string : Frama_c_kernel.Base.cstring -> string Mt_lib.conversion
Sourceval int_to_value : int -> Types.value
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct