package frama-c

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

Install

Dune Dependency

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

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. L
    Loïc Correnson
  16. J
    Julien Crétin
  17. P
    Pascal Cuoq
  18. Z
    Zaynah Dargaye
  19. B
    Basile Desloges
  20. J
    Jean-Christophe Filliâtre
  21. P
    Philippe Herrmann
  22. M
    Maxime Jacquemin
  23. F
    Florent Kirchner
  24. A
    Alexander Kogtenkov
  25. R
    Remi Lazarini
  26. T
    Tristan Le Gall
  27. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Structural_descr/index.html

Module Frama_c_kernel.Structural_descr

Internal representations of OCaml type as first class values. These values are called structural descriptors.

  • since Carbon-20101201

Type declarations

type recursive

Type used for handling (possibly mutually) recursive structural descriptors. See module Recursive.

type single_pack = private Unmarshal.t
type pack = private
  1. | Nopack
    (*

    Was impossible to build a pack.

    *)
  2. | Pack of single_pack
    (*

    A standard pack.

    *)
  3. | Recursive of recursive
    (*

    Pack for a recursive descriptor. See module Recursive.

    *)

Structural descriptor used inside structures.

type t = private
  1. | Unknown
    (*

    Use it either for unmarshable types or if you don't know its internal representation. In any case, values of types with this descriptor will never be written on disk.

    *)
  2. | Abstract
    (*

    The data is marshable as an usual OCaml value. No specific processing will be applied on any part of such a data.

    *)
  3. | Structure of structure
    (*

    Provide a description of the representation of data.

    *)
  4. | T_pack of single_pack
    (*

    Internal use only. Do not use it outside the library

    *)

Type of internal representations of OCaml type.

Example: the structural descriptor of A | B of int * bool | C of string is Structure (Sum [| [| p_int; p_bool |]; [| p_string |] |]). Ok, in this case, just Abstract is valid too.

and structure = private
  1. | Sum of pack array array
    (*

    Sum c describes a non-array type where c is an array describing the non-constant constructors of the type being described (in the order of their declarations in that type). Each element of this latter array is an array of t that describes (in order) the fields of the corresponding constructor.

    *)
  2. | Array of pack
    (*

    The data is an array of values of the same type, each value being described by the pack.

    *)

Description with details.

Pack builders

val pack : t -> pack

Pack a structural descriptor in order to embed it inside another one.

val recursive_pack : recursive -> pack

Pack a recursive descriptor.

  • since Nitrogen-20111001
module Recursive : sig ... end

Use this module for handling a (possibly recursive) structural descriptor d. Call Recursive.create () (returning r) before building d. Build d and use Recursive r in places where d should be put. Call Recursive.update r d after building d.

Predefined descriptors

val t_unknown : t
  • since Neon-20140301
val t_abstract : t
  • since Neon-20140301
val t_unit : t
val t_int : t
val t_string : t
val t_float : t
val t_bool : t
val t_int32 : t
val t_int64 : t
val t_nativeint : t
val t_record : pack array -> t
val t_tuple : pack array -> t
val t_list : t -> t
val t_ref : t -> t
val t_option : t -> t
val t_array : t -> t
val t_queue : t -> t
val t_sum : pack array array -> t
  • since Neon-20140301

Use the functions below only if the compare/hash functions cannot change by marshalling.

val t_set_unchanged_compares : t -> t
val t_map_unchanged_compares : t -> t -> t
val t_hashtbl_unchanged_hashs : t -> t -> t

Packed versions of predefined descriptors.

val p_abstract : pack

Equivalent to pack Abstract

val p_unit : pack
val p_int : pack
val p_string : pack
val p_float : pack
val p_bool : pack
val p_int32 : pack
val p_int64 : pack
val p_nativeint : pack

Internals

These values must be used only inside the Type library.

exception Cannot_pack
val unsafe_pack : Unmarshal.t -> pack
val of_pack : single_pack -> t
val cleanup : t -> t
val are_consistent : t -> t -> bool

Not symmetrical: check that the second argument is a correct refinement of the first one.

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