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. | FLOAT
  105. | FALSE
  106. | EXT_SPEC_MODULE
  107. | EXT_SPEC_LET
  108. | EXT_SPEC_INCLUDE
  109. | EXT_SPEC_FUNCTION
  110. | EXT_SPEC_CONTRACT
  111. | EXT_SPEC_AT
  112. | EXT_LOADER_PLUGIN of string * string
  113. | EXT_LOADER of string * string
  114. | EXT_GLOBAL_BLOCK of string * string
  115. | EXT_GLOBAL of string * string
  116. | EXT_CONTRACT of string * string
  117. | EXT_CODE_ANNOT of string * string
  118. | EXITS
  119. | EXISTS
  120. | EQUAL
  121. | EQ
  122. | EOF
  123. | ENUM
  124. | ENSURES
  125. | EMPTY
  126. | ELSE
  127. | DYNAMIC
  128. | DOUBLE
  129. | DOTDOTDOT
  130. | DOTDOT
  131. | DOT
  132. | DOLLAR
  133. | DISJOINT
  134. | DECREASES
  135. | DANGLING
  136. | CONTINUES
  137. | CONST
  138. | COMPLETE
  139. | COMMA
  140. | COLONCOLON
  141. | COLON2
  142. | COLON
  143. | CHECK_RETURNS
  144. | CHECK_REQUIRES
  145. | CHECK_LOOP
  146. | CHECK_LEMMA
  147. | CHECK_INVARIANT
  148. | CHECK_EXITS
  149. | CHECK_ENSURES
  150. | CHECK_CONTINUES
  151. | CHECK_BREAKS
  152. | CHECK
  153. | CHAR
  154. | CASE
  155. | BSUNION
  156. | BSTYPE
  157. | BREAKS
  158. | BOOLEAN
  159. | BOOL
  160. | BLOCK_LENGTH
  161. | BIMPLIES
  162. | BIFF
  163. | BEHAVIORS
  164. | BEHAVIOR
  165. | BASE_ADDR
  166. | AXIOMATIC
  167. | AXIOM
  168. | AUTOMATIC
  169. | AT
  170. | ASSUMES
  171. | ASSIGNS
  172. | ASSERT
  173. | AS
  174. | ARROW
  175. | AND
  176. | AMP
  177. | ALLOCATION
  178. | ALLOCATES
  179. | ALLOCABLE
  180. | ADMIT_RETURNS
  181. | ADMIT_REQUIRES
  182. | ADMIT_LOOP
  183. | ADMIT_LEMMA
  184. | ADMIT_INVARIANT
  185. | ADMIT_EXITS
  186. | ADMIT_ENSURES
  187. | ADMIT_CONTINUES
  188. | ADMIT_BREAKS
  189. | 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