package frama-c

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

The module stores the current file,line, and working directory in a hidden internal state, modified by the three following functions.

val newline : unit -> unit

Call this function to announce a new line

val currentLoc : unit -> Cil_datatype.Location.t
val setCurrentWorkingDirectory : string -> unit

This function is used especially when the preprocessor has generated linemarkers in the output that let us know the current working directory at the time of preprocessing (option -fworking-directory for GNU CPP).

val setCurrentFile : string -> unit
val setCurrentLine : int -> unit
val startParsing : string -> (Stdlib.Lexing.lexbuf -> 'a) -> Stdlib.Lexing.lexbuf * (Stdlib.Lexing.lexbuf -> 'a)

Call this function to start parsing.

val finishParsing : unit -> unit

Call this function to finish parsing and close the input channel

val pp_context_from_file : ?ctx:int -> ?start_line:int -> Stdlib.Format.formatter -> Filepath.position -> unit

prints the line identified by the position, together with ctx lines of context before and after. ctx defaults to 2. If start_line is specified, then all lines between start_line and pos.pos_lnum are considered part of the error.

val pp_location : Stdlib.Format.formatter -> Cil_types.location -> unit

prints a readable description of a location

  • since 22.0-Titanium
val parse_error : ?source:Filepath.position -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Emits the corresponding error message with some location information. If given, source will be treated as the last position of the offending expression that led to the error. It defaults to the current position of the lexbuf currently in use (i.e. startParsing must have been called before that, and no finishParsing call must have been done in between). The start position will be inferred from menhir's error reporting mecanisms.

val had_errors : unit -> bool

Has an error been raised since the last call to clear_errors?

val clear_errors : unit -> unit

Parse errors are usually fatal, but their reporting is sometimes delayed until the end of the current parsing phase. Functions that intend to ultimately fail should call clear_errors when they start, and check had_errors when they end, then call parse_error if needed.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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