Frama-C:
Plug-ins:
Libraries:

Frama-C API - Logic_lexer

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 ext_spec : Stdlib.Lexing.lexbuf -> Logic_ptree.ext_spec

ACSL extension for parsing external spec file. Modifies tokens as follows:

  • C-comments /* ... */ can be used and can be nested
  • "module" keyword is interpreted as EXT_SPEC_MODULE