sig
type token =
MODULE
| FUNCTION
| CONTRACT
| INCLUDE
| EXT_AT
| EXT_LET
| IDENTIFIER of string
| TYPENAME of string
| STRING_LITERAL of (bool * string)
| INT_CONSTANT of string
| FLOAT_CONSTANT of string
| STRING_CONSTANT of string
| WSTRING_CONSTANT of string
| LPAR
| RPAR
| IF
| ELSE
| COLON
| COLON2
| COLONCOLON
| DOT
| DOTDOT
| DOTDOTDOT
| INT
| INTEGER
| REAL
| BOOLEAN
| BOOL
| FLOAT
| LT
| GT
| LE
| GE
| EQ
| NE
| COMMA
| ARROW
| EQUAL
| FORALL
| EXISTS
| IFF
| IMPLIES
| AND
| OR
| NOT
| SEPARATED
| TRUE
| FALSE
| OLD
| AT
| RESULT
| BLOCK_LENGTH
| BASE_ADDR
| OFFSET
| VALID
| VALID_READ
| VALID_INDEX
| VALID_RANGE
| OBJECT_POINTER
| VALID_FUNCTION
| ALLOCATION
| STATIC
| REGISTER
| AUTOMATIC
| DYNAMIC
| UNALLOCATED
| ALLOCABLE
| FREEABLE
| FRESH
| DOLLAR
| QUESTION
| MINUS
| PLUS
| STAR
| AMP
| SLASH
| PERCENT
| LSQUARE
| RSQUARE
| EOF
| GLOBAL
| INVARIANT
| VARIANT
| DECREASES
| FOR
| LABEL
| ASSERT
| CHECK
| ADMIT
| SEMICOLON
| NULL
| EMPTY
| REQUIRES
| ENSURES
| ALLOCATES
| FREES
| ASSIGNS
| LOOP
| NOTHING
| SLICE
| IMPACT
| PRAGMA
| FROM
| CHECK_REQUIRES
| CHECK_LOOP
| CHECK_INVARIANT
| CHECK_LEMMA
| CHECK_ENSURES
| CHECK_EXITS
| CHECK_CONTINUES
| CHECK_BREAKS
| CHECK_RETURNS
| ADMIT_REQUIRES
| ADMIT_LOOP
| ADMIT_INVARIANT
| ADMIT_LEMMA
| ADMIT_ENSURES
| ADMIT_EXITS
| ADMIT_CONTINUES
| ADMIT_BREAKS
| ADMIT_RETURNS
| EXT_CODE_ANNOT of string
| EXT_GLOBAL of string
| EXT_GLOBAL_BLOCK of string
| EXT_CONTRACT of string
| EXITS
| BREAKS
| CONTINUES
| RETURNS
| VOLATILE
| READS
| WRITES
| LOGIC
| PREDICATE
| INDUCTIVE
| AXIOMATIC
| AXIOM
| LEMMA
| LBRACE
| RBRACE
| GHOST
| MODEL
| CASE
| VOID
| CHAR
| SIGNED
| UNSIGNED
| SHORT
| LONG
| DOUBLE
| STRUCT
| ENUM
| UNION
| BSUNION
| INTER
| TYPE
| BEHAVIOR
| BEHAVIORS
| ASSUMES
| COMPLETE
| DISJOINT
| TERMINATES
| BIFF
| BIMPLIES
| STARHAT
| HAT
| HATHAT
| PIPE
| TILDE
| GTGT
| LTLT
| SIZEOF
| LAMBDA
| LET
| TYPEOF
| BSTYPE
| WITH
| CONST
| INITIALIZED
| DANGLING
| CUSTOM
| LSQUAREPIPE
| RSQUAREPIPE
| IN
| PI
val lexpr_eof :
(Stdlib.Lexing.lexbuf -> Logic_parser.token) ->
Stdlib.Lexing.lexbuf -> Logic_ptree.lexpr
val annot :
(Stdlib.Lexing.lexbuf -> Logic_parser.token) ->
Stdlib.Lexing.lexbuf -> Logic_ptree.annot
val spec :
(Stdlib.Lexing.lexbuf -> Logic_parser.token) ->
Stdlib.Lexing.lexbuf -> Logic_ptree.spec
val ext_spec :
(Stdlib.Lexing.lexbuf -> Logic_parser.token) ->
Stdlib.Lexing.lexbuf -> Logic_ptree.ext_spec
end