package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. F
    Fabien Siron
  55. N
    Nicolas Stouls
  56. H
    Hugo Thievenaz
  57. K
    Kostyantyn Vorobyov
  58. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-32.0-beta-Germanium.tar.gz
sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3

doc/mthread/Mthread/Mt_memory/index.html

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