package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.