module Logic_lexer:sig..end
Lexer for logic annotations
val token : Stdlib.Lexing.lexbuf -> Logic_parser.tokenFor plugins that need to call functions of Logic_parser themselves
val chr : Stdlib.Lexing.lexbuf -> string
val is_acsl_keyword : string -> bool
type'aparse =Filepath.position * string -> (Filepath.position * 'a) option
Generic type for parsing functions built on tip of the lexer. Given
such a function f, f (pos, s) parses s, assuming that it starts at
position pos. If parsing is successful, it returns the final position,
and the result. If an error occurs with a warning status other than Wabort
for annot-error, returns None
val lexpr : Logic_ptree.lexpr parse
val annot : Logic_ptree.annot parse
val spec : Logic_ptree.spec parse
val ext_spec : Stdlib.Lexing.lexbuf -> Logic_ptree.ext_specACSL extension for parsing external spec file. Here, the tokens "/*" and "*/" are accepted by the lexer as unnested C comments into the external ACSL specifications.