package frama-c

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