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/frama-c.kernel/Frama_c_kernel/Nat/index.html

Module Frama_c_kernel.Nat

Encoding of the Peano arithmetic in OCaml type system. A value of type n nat contains n at the value and the type level, allowing to express properties on objects sizes and accesses for example. It is used by the module Linear to represent vectors and matrices dimensions.

type zero = |
type 'n succ = |
type 'n nat
type positive_or_null =
  1. | PositiveOrNull : 'n nat -> positive_or_null
type strictly_positive =
  1. | StrictlyPositive : 'n succ nat -> strictly_positive
val zero : zero nat
val one : zero succ nat
val succ : 'n nat -> 'n succ nat
val prev : 'n succ nat -> 'n nat
val to_int : 'n nat -> int

The call to_int n returns an integer equal to n. This function complexity is O(1).

val of_int : int -> positive_or_null option

Returns a positive or null natural. If the given parameter is strictly negative then None is returned. This function complexity is O(1).

val of_strictly_positive_int : int -> strictly_positive option

Returns a strictly positive natural. If the given parameter is less or equal than zero, then None is returned. This function complexity is O(1).