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. | 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_EXT of string
  90. | IDENTIFIER of string
  91. | HATHAT
  92. | HAT
  93. | GTGT
  94. | GT
  95. | GLOBAL
  96. | GHOST
  97. | GE
  98. | FUNCTION
  99. | FROM
  100. | FRESH
  101. | FREES
  102. | FREEABLE
  103. | FORALL
  104. | FOR
  105. | FLOAT_CONSTANT of string
  106. | FLOAT
  107. | FALSE
  108. | EXT_LET
  109. | EXT_GLOBAL_BLOCK of string
  110. | EXT_GLOBAL of string
  111. | EXT_CONTRACT of string
  112. | EXT_CODE_ANNOT of string
  113. | EXT_AT
  114. | EXITS
  115. | EXISTS
  116. | EQUAL
  117. | EQ
  118. | EOF
  119. | ENUM
  120. | ENSURES
  121. | EMPTY
  122. | ELSE
  123. | DYNAMIC
  124. | DOUBLE
  125. | DOTDOTDOT
  126. | DOTDOT
  127. | DOT
  128. | DOLLAR
  129. | DISJOINT
  130. | DECREASES
  131. | DANGLING
  132. | CONTRACT
  133. | CONTINUES
  134. | CONST
  135. | COMPLETE
  136. | COMMA
  137. | COLONCOLON
  138. | COLON2
  139. | COLON
  140. | CHECK_RETURNS
  141. | CHECK_REQUIRES
  142. | CHECK_LOOP
  143. | CHECK_LEMMA
  144. | CHECK_INVARIANT
  145. | CHECK_EXITS
  146. | CHECK_ENSURES
  147. | CHECK_CONTINUES
  148. | CHECK_BREAKS
  149. | CHECK
  150. | CHAR
  151. | CASE
  152. | BSUNION
  153. | BSTYPE
  154. | BSGHOST
  155. | BREAKS
  156. | BOOLEAN
  157. | BOOL
  158. | BLOCK_LENGTH
  159. | BIMPLIES
  160. | BIFF
  161. | BEHAVIORS
  162. | BEHAVIOR
  163. | BASE_ADDR
  164. | AXIOMATIC
  165. | AXIOM
  166. | AUTOMATIC
  167. | AT
  168. | ASSUMES
  169. | ASSIGNS
  170. | ASSERT
  171. | ARROW
  172. | AND
  173. | AMP
  174. | ALLOCATION
  175. | ALLOCATES
  176. | ALLOCABLE
  177. | ADMIT_RETURNS
  178. | ADMIT_REQUIRES
  179. | ADMIT_LOOP
  180. | ADMIT_LEMMA
  181. | ADMIT_INVARIANT
  182. | ADMIT_EXITS
  183. | ADMIT_ENSURES
  184. | ADMIT_CONTINUES
  185. | ADMIT_BREAKS
  186. | 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