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/Finite/index.html

Module Frama_c_kernel.Finite

Encoding of finite set in OCaml type system.

type 'n finite

The type n finite encodes all finite sets of cardinal n. It is used by the module Linear to represent accesses to vectors and matrices coefficients, statically ensuring that no out of bounds access can be performed.

val first : 'n Nat.succ finite

The first element of any finite subset. The type encodes that for a finite subset to have an element, its cardinal must be at least one.

val last : 'n Nat.succ Nat.nat -> 'n Nat.succ finite

last n returns a value encoding the last element of any finite subset of cardinal n.

val next : 'n finite -> 'n Nat.succ finite

The call next f returns a value encoding the element right after f in a finite subset. The type encodes the relations between the cardinal of the finite subset containing f and the cardinal of the one containing its successor.

val prev : 'n Nat.succ finite -> 'n finite

The call prev f returns a value encoding the element right before f in a finite subset. The type encodes the relations between the cardinal of the finite subset containing f and the cardinal of the one containing its predecessor.

val weaken : 'n finite -> 'n Nat.succ finite

If f is an element of any finite subset of cardinal n, it is also an element of any finite subset of cardinal n + 1. The call weaken f allows to prove that fact to the type system.

val strengthen : 'n Nat.nat -> 'n Nat.succ finite -> 'n finite option

If f is an element of any finite subset of cardinal n + 1, it may also be an element of any finite subset of cardinal n. The call strengthen n f allows to prove that fact to the type system. None is returned if and only if f is the last element of its subset.

val of_int : 'n Nat.succ Nat.nat -> int -> 'n Nat.succ finite option

The call of_int limit n returns a finite value representing the nth element of a finite set of cardinal limit. If n is not in the bounds, None is returned. This function complexity is O(1).

val to_int : 'n finite -> int

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

val for_each : ('n finite -> 'a -> 'a) -> 'n Nat.nat -> 'a -> 'a

The call for_each f limit acc folds over each finite elements of a set of cardinal limit, computing f at each step. The function complexity is O(n).

Relational operators.

val (=) : 'n finite -> 'n finite -> bool
val (!=) : 'n finite -> 'n finite -> bool
val (<) : 'n finite -> 'n finite -> bool
val (<=) : 'n finite -> 'n finite -> bool
val (>) : 'n finite -> 'n finite -> bool
val (>=) : 'n finite -> 'n finite -> bool

Deprecated definitions.

val strenghten : 'n Nat.nat -> 'n Nat.succ finite -> 'n finite option

If f is an element of any finite subset of cardinal n + 1, it may also be an element of any finite subset of cardinal n. The call strenghten n f allows to prove that fact to the type system. None is returned if and only if f is the last element of its subset.

  • deprecated Use strengthen instead.