Module Logic_lexer

module Logic_lexer: sig .. end

Lexer for logic annotations


val token : Stdlib.Lexing.lexbuf -> Logic_parser.token

For plugins that need to call functions of Logic_parser themselves

val chr : Stdlib.Lexing.lexbuf -> string
val is_acsl_keyword : string -> bool
type 'a parse = 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_spec

ACSL extension for parsing external spec file. Here, the tokens "/*" and "*/" are accepted by the lexer as unnested C comments into the external ACSL specifications.