Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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. | STAR_EQ
  26. | STARHAT
  27. | STAR
  28. | SLASH_EQ
  29. | SLASH
  30. | SIZEOF
  31. | SIGNED
  32. | SHORT
  33. | SEPARATED
  34. | SEMICOLON
  35. | RSQUAREPIPE
  36. | RSQUARE
  37. | RPAR
  38. | RETURNS
  39. | RESULT
  40. | REQUIRES
  41. | REGISTER
  42. | REAL
  43. | READS
  44. | RBRACE
  45. | RARROW
  46. | QUESTION
  47. | PREDICATE
  48. | PLUS_EQ
  49. | PLUS
  50. | PIPE_EQ
  51. | PIPE
  52. | PI
  53. | PERCENT_EQ
  54. | PERCENT
  55. | OR
  56. | OLD
  57. | OFFSET
  58. | OBJECT_POINTER
  59. | NULL
  60. | NOTHING
  61. | NOT
  62. | NE
  63. | MODULE
  64. | MODEL
  65. | MINUS_EQ
  66. | MINUS
  67. | LTLT
  68. | LT
  69. | LSQUAREPIPE
  70. | LSQUARE
  71. | LPAR
  72. | LOOP
  73. | LONGIDENT of string
  74. | LONG
  75. | LOGIC
  76. | LET
  77. | LEMMA
  78. | LE
  79. | LBRACE
  80. | LARROW
  81. | LAMBDA
  82. | LABEL
  83. | INVARIANT
  84. | INT_CONSTANT of string
  85. | INTER
  86. | INTEGER
  87. | INT
  88. | INITIALIZED
  89. | INDUCTIVE
  90. | IN
  91. | IMPORT
  92. | IMPLIES
  93. | IFF
  94. | IF
  95. | IDENTIFIER_LOADER of string
  96. | IDENTIFIER_EXT of string
  97. | IDENTIFIER of string
  98. | HATHAT
  99. | HAT
  100. | GTGT
  101. | GT
  102. | GLOBAL
  103. | GHOST
  104. | GE
  105. | FROM
  106. | FRESH
  107. | FREES
  108. | FREEABLE
  109. | FORALL
  110. | FOR
  111. | FLOAT_CONSTANT of string
  112. | FLOAT64
  113. | FLOAT32
  114. | FLOAT
  115. | FALSE
  116. | EXT_SPEC_MODULE
  117. | EXT_SPEC_LET
  118. | EXT_SPEC_INCLUDE
  119. | EXT_SPEC_FUNCTION
  120. | EXT_SPEC_CONTRACT
  121. | EXT_SPEC_AT
  122. | EXT_LOADER_PLUGIN of string * string
  123. | EXT_LOADER of string * string
  124. | EXT_GLOBAL_BLOCK of string * string
  125. | EXT_GLOBAL of string * string
  126. | EXT_CONTRACT of string * string
  127. | EXT_CODE_ANNOT of string * string
  128. | EXITS
  129. | EXISTS
  130. | EQUAL
  131. | EQ
  132. | EOF
  133. | ENUM
  134. | ENSURES
  135. | EMPTY
  136. | ELSE
  137. | DYNAMIC
  138. | DOUBLE
  139. | DOTDOTDOT
  140. | DOTDOT
  141. | DOT
  142. | DOLLAR
  143. | DISJOINT
  144. | DECREASES
  145. | DANGLING
  146. | CONTINUES
  147. | CONST
  148. | COMPLETE
  149. | COMMA
  150. | COLON_EQ
  151. | COLONCOLON
  152. | COLON2
  153. | COLON
  154. | CIRC_EQ
  155. | CHECK_RETURNS
  156. | CHECK_REQUIRES
  157. | CHECK_LOOP
  158. | CHECK_LEMMA
  159. | CHECK_INVARIANT
  160. | CHECK_EXITS
  161. | CHECK_ENSURES
  162. | CHECK_CONTINUES
  163. | CHECK_BREAKS
  164. | CHECK
  165. | CHAR
  166. | CASE
  167. | BSUNION
  168. | BSTYPE
  169. | BREAKS
  170. | BOOLEAN
  171. | BOOL
  172. | BLOCK_LENGTH
  173. | BIMPLIES
  174. | BIFF
  175. | BEHAVIORS
  176. | BEHAVIOR
  177. | BASE_ADDR
  178. | AXIOMATIC
  179. | AXIOM
  180. | AUTOMATIC
  181. | AT
  182. | ASSUMES
  183. | ASSIGNS
  184. | ASSERT
  185. | AS
  186. | AND_EQ
  187. | AND
  188. | AMP
  189. | ALLOCATION
  190. | ALLOCATES
  191. | ALLOCABLE
  192. | ALIGNOF
  193. | ALIGNED
  194. | ADMIT_RETURNS
  195. | ADMIT_REQUIRES
  196. | ADMIT_LOOP
  197. | ADMIT_LEMMA
  198. | ADMIT_INVARIANT
  199. | ADMIT_EXITS
  200. | ADMIT_ENSURES
  201. | ADMIT_CONTINUES
  202. | ADMIT_BREAKS
  203. | ADMIT
exception Error
val spec : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.spec
val lexpr_list_eof : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Logic_ptree.lexpr list
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