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