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 (25)

Authors

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

Maintainers

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

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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.