package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.kernel/Frama_c_kernel/Errorloc/index.html

Module `Frama_c_kernel.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 ->
  (Lexing.lexbuf -> 'a) ->
  Lexing.lexbuf * (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 ->
  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 : Format.formatter -> Cil_types.location -> unit

prints a readable description of a location

since 22.0-Titanium

val parse_error : 
  ?source:Filepath.position ->
  ('a, Format.formatter, unit, 'b) 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.