package frama-c

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct