sig
type token =
MODULE
| FUNCTION
| CONTRACT
| INCLUDE
| EXT_AT
| EXT_LET
| IDENTIFIER of string
| TYPENAME of string
| STRING_LITERAL of (bool * string)
| CONSTANT of Logic_ptree.constant
| CONSTANT10 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
| 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
| SEMICOLON
| NULL
| EMPTY
| REQUIRES
| ENSURES
| ALLOCATES
| FREES
| ASSIGNS
| LOOP
| NOTHING
| SLICE
| IMPACT
| PRAGMA
| FROM
| 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
| LTCOLON
| COLONGT
| TYPE
| BEHAVIOR
| BEHAVIORS
| ASSUMES
| COMPLETE
| DISJOINT
| TERMINATES
| BIFF
| BIMPLIES
| HAT
| HATHAT
| PIPE
| TILDE
| GTGT
| LTLT
| SIZEOF
| LAMBDA
| LET
| TYPEOF
| BSTYPE
| WITH
| CONST
| INITIALIZED
| DANGLING
| CUSTOM
val lexpr_eof :
(Lexing.lexbuf -> Logic_parser.token) ->
Lexing.lexbuf -> Logic_ptree.lexpr
val annot :
(Lexing.lexbuf -> Logic_parser.token) ->
Lexing.lexbuf -> Logic_ptree.annot
val spec :
(Lexing.lexbuf -> Logic_parser.token) ->
Lexing.lexbuf -> Logic_ptree.spec
val ext_spec :
(Lexing.lexbuf -> Logic_parser.token) ->
Lexing.lexbuf -> Logic_ptree.ext_spec
end