package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
val spec : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.spec
val lexpr_eof : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.lexpr
val ext_spec : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.ext_spec
val annot : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.annot
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