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 currentLoc : unit -> Cil_datatype.Location.t
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 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
val parse_error :
?source:Filepath.position ->
( 'a, Stdlib.Format.formatter, unit, 'b ) Stdlib.format4 ->
'a
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.
Has an error been raised since the last call to clear_errors
?