Module Frama_c_kernel.Logic_lexer

Lexer for logic annotations

For plugins that need to call functions of Logic_parser themselves

val chr : 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

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.