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