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

Module Frama_c_kernel.Logic_parser

type token =
  1. | WSTRING_CONSTANT of string
  2. | WRITES
  3. | WITH
  4. | VOLATILE
  5. | VOID
  6. | VARIANT
  7. | VALID_READ
  8. | VALID_RANGE
  9. | VALID_INDEX
  10. | VALID_FUNCTION
  11. | VALID
  12. | UNSIGNED
  13. | UNION
  14. | UNALLOCATED
  15. | TYPEOF
  16. | TYPENAME of string
  17. | TYPE
  18. | TRUE
  19. | TILDE
  20. | TERMINATES
  21. | STRUCT
  22. | STRING_LITERAL of bool * string
  23. | STRING_CONSTANT of string
  24. | STATIC
  25. | STARHAT
  26. | STAR
  27. | SLICE
  28. | SLASH
  29. | SIZEOF
  30. | SIGNED
  31. | SHORT
  32. | SEPARATED
  33. | SEMICOLON
  34. | RSQUAREPIPE
  35. | RSQUARE
  36. | RPAR
  37. | RETURNS
  38. | RESULT
  39. | REQUIRES
  40. | REGISTER
  41. | REAL
  42. | READS
  43. | RBRACE
  44. | QUESTION
  45. | PREDICATE
  46. | PRAGMA
  47. | PLUS
  48. | PIPE
  49. | PI
  50. | PERCENT
  51. | OR
  52. | OLD
  53. | OFFSET
  54. | OBJECT_POINTER
  55. | NULL
  56. | NOTHING
  57. | NOT
  58. | NE
  59. | MODULE
  60. | MODEL
  61. | MINUS
  62. | LTLT
  63. | LT
  64. | LSQUAREPIPE
  65. | LSQUARE
  66. | LPAR
  67. | LOOP
  68. | LONG
  69. | LOGIC
  70. | LET
  71. | LEMMA
  72. | LE
  73. | LBRACE
  74. | LAMBDA
  75. | LABEL
  76. | INVARIANT
  77. | INT_CONSTANT of string
  78. | INTER
  79. | INTEGER
  80. | INT
  81. | INITIALIZED
  82. | INDUCTIVE
  83. | INCLUDE
  84. | IN
  85. | IMPLIES
  86. | IMPACT
  87. | IFF
  88. | IF
  89. | IDENTIFIER of string
  90. | HATHAT
  91. | HAT
  92. | GTGT
  93. | GT
  94. | GLOBAL
  95. | GHOST
  96. | GE
  97. | FUNCTION
  98. | FROM
  99. | FRESH
  100. | FREES
  101. | FREEABLE
  102. | FORALL
  103. | FOR
  104. | FLOAT_CONSTANT of string
  105. | FLOAT
  106. | FALSE
  107. | EXT_LET
  108. | EXT_GLOBAL_BLOCK of string
  109. | EXT_GLOBAL of string
  110. | EXT_CONTRACT of string
  111. | EXT_CODE_ANNOT of string
  112. | EXT_AT
  113. | EXITS
  114. | EXISTS
  115. | EQUAL
  116. | EQ
  117. | EOF
  118. | ENUM
  119. | ENSURES
  120. | EMPTY
  121. | ELSE
  122. | DYNAMIC
  123. | DOUBLE
  124. | DOTDOTDOT
  125. | DOTDOT
  126. | DOT
  127. | DOLLAR
  128. | DISJOINT
  129. | DECREASES
  130. | DANGLING
  131. | CONTRACT
  132. | CONTINUES
  133. | CONST
  134. | COMPLETE
  135. | COMMA
  136. | COLONCOLON
  137. | COLON2
  138. | COLON
  139. | CHECK_RETURNS
  140. | CHECK_REQUIRES
  141. | CHECK_LOOP
  142. | CHECK_LEMMA
  143. | CHECK_INVARIANT
  144. | CHECK_EXITS
  145. | CHECK_ENSURES
  146. | CHECK_CONTINUES
  147. | CHECK_BREAKS
  148. | CHECK
  149. | CHAR
  150. | CASE
  151. | BSUNION
  152. | BSTYPE
  153. | BSGHOST
  154. | BREAKS
  155. | BOOLEAN
  156. | BOOL
  157. | BLOCK_LENGTH
  158. | BIMPLIES
  159. | BIFF
  160. | BEHAVIORS
  161. | BEHAVIOR
  162. | BASE_ADDR
  163. | AXIOMATIC
  164. | AXIOM
  165. | AUTOMATIC
  166. | AT
  167. | ASSUMES
  168. | ASSIGNS
  169. | ASSERT
  170. | ARROW
  171. | AND
  172. | AMP
  173. | ALLOCATION
  174. | ALLOCATES
  175. | ALLOCABLE
  176. | ADMIT_RETURNS
  177. | ADMIT_REQUIRES
  178. | ADMIT_LOOP
  179. | ADMIT_LEMMA
  180. | ADMIT_INVARIANT
  181. | ADMIT_EXITS
  182. | ADMIT_ENSURES
  183. | ADMIT_CONTINUES
  184. | ADMIT_BREAKS
  185. | ADMIT
exception Error