Frama-C:
Plug-ins:
Libraries:

Frama-C API - Errorloc

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 -> Stdlib.Format.formatter -> Cil_types.location -> unit

prints the line(s) identified by the location, together with ctx lines of context before and after. ctx defaults to 2. If the location expands to multiple lines, those lines will be separated from context by blank lines. Otherwise, the portion of the line that is between the two positions of the location will be underlined with ^ NB: if the two positions in the location refer to different files, the first position will not be considered.

  • before 29.0-Copper:

    the function took as argument a single position and and an optional start_line (as an int) to indicate a different starting line.

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

prints a readable description of a location

  • since 22.0-Titanium
val parse_error : ?loc:Cil_types.location -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

Emits the corresponding error message with some location information. If not given, location will be considered to be between the end of the forelast token read by the parser and the start of the last token, i.e. we assume the parser has read an unexpected token.

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.