package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/mthread/Mthread/Mt_memory/index.html

Module `Mthread.Mt_memory`Source

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

Source

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

Source

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.

Source

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.

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

Conversion to and from Mthread world to the value analysis

Source

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

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

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

Source

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

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

Source

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

Sourceval int_to_value : int -> Types.value

Sourceval pretty_slice : Types.slice Frama_c_kernel.Pretty_utils.formatter

On This Page

Union of state, values and list of values
Reading and writing in memory
Conversion to and from Mthread world to the value analysis

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mthread/Mthread/Mt_memory/index.html

Module Mthread.Mt_memorySource

Union of state, values and list of values

Reading and writing in memory

Conversion to and from Mthread world to the value analysis

Module `Mthread.Mt_memory`Source