diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index 8a7715c735a951af17a0b4c90efc3c034f9cbbcd..9d1e3669dce6fe5e0e3fada852afb769d27be3f0 100644
--- a/src/kernel_internals/parsing/errorloc.ml
+++ b/src/kernel_internals/parsing/errorloc.ml
@@ -138,23 +138,24 @@ let setCurrentFile n =
}
end
-(* Prints the [pos.pos_lnum]-th line from file [pos.pos_fname],
- plus up to [ctx] lines before and after [pos.pos_lnum] (if they exist),
- similar to 'grep -C<ctx>'. The first line is numbered 1.
+(* Prints the line(s) between start_pos and pos,
+ plus up to [ctx] lines before and after (if they exist),
+ similar to 'grep -C<ctx>'.
Most exceptions are silently caught and printing is stopped if they occur. *)
-let pp_context_from_file ?(ctx=2) ?start_pos fmt pos =
+let pp_context_from_file ?(ctx=2) fmt (start_pos, pos) =
+ let open Filepath in
try
- let in_ch = open_in (pos.Filepath.pos_path :> string) in
+ let start_pos =
+ if Normalized.equal start_pos.pos_path pos.pos_path then start_pos
+ else pos
+ in
+ let in_ch = open_in (pos.pos_path :> string) in
try
begin
- let open Filepath in
let first_error_line, start_char, last_error_line =
- match start_pos with
- | None -> pos.pos_lnum, 1, pos.pos_lnum
- | Some s ->
- min s.pos_lnum pos.pos_lnum,
- (s.pos_cnum - s.pos_bol + 1),
- max s.pos_lnum pos.pos_lnum
+ min start_pos.pos_lnum pos.pos_lnum,
+ (start_pos.pos_cnum - start_pos.pos_bol + 1),
+ max start_pos.pos_lnum pos.pos_lnum
in
(* The difference between the first and last error lines can be very
large; in this case, we print only the first and last [error_ctx]
@@ -265,9 +266,9 @@ let parse_error ?loc msg =
ignore (MenhirLib.ErrorReports.show pp current.menhir_pos)
with _ -> ()
in
- let start_pos,last_pos =
+ let loc =
match loc with
- | Some (s,l) -> s, l
+ | Some loc -> loc
| None ->
if Stack.is_empty all_pos then
Cil_datatype.Location.of_lexing_loc
@@ -292,13 +293,13 @@ let parse_error ?loc msg =
Format.fprintf fmt ", before or at token: %s" token
in
Pretty_utils.ksfprintf (fun str ->
- Kernel.feedback ~source:start_pos "%s:@." str
+ Kernel.feedback ~source:(fst loc) "%s:@." str
~append:(fun fmt ->
Format.fprintf fmt "%a%a\n"
- pp_location (start_pos, last_pos)
+ pp_location loc
pretty_token (Lexing.lexeme current.lexbuf);
Format.fprintf fmt "%a@."
- (pp_context_from_file ~start_pos ~ctx:2) last_pos);
+ (pp_context_from_file ~ctx:2) loc);
raise (Log.AbortError "kernel"))
msg
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index 2dba434819b48748445ea90f6c6c481c8e6a1965..a83180cd21bda8a38594036ed6a639aae1949399 100644
--- a/src/kernel_internals/parsing/errorloc.mli
+++ b/src/kernel_internals/parsing/errorloc.mli
@@ -66,18 +66,20 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and
close the input channel *)
-(** prints the line identified by the position, together with [ctx] lines
+(** prints the line(s) identified by the location, together with [ctx] lines
of context before and after. [ctx] defaults to 2.
- If [start_pos] is specified, then all positions between [start_pos] and
- [pos] are considered part of the error. If this 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
- will be underlined with [^]
- @before Frama-C+dev: [start_pos] was named [start_line] (and was an [int]).
+ 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 Frama-C+dev: 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_context_from_file:
- ?ctx:int -> ?start_pos:Filepath.position ->
- Format.formatter -> Filepath.position -> unit
+ ?ctx:int -> Format.formatter -> Cil_types.location -> unit
(** prints a readable description of a location
@since 22.0-Titanium *)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4e6412b2e889cac067075e4c61d75eef677c7a3b..613d5ee148de1b13ebb7fb05591c2b75dff9b1a7 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -132,10 +132,9 @@ let abort_context ?loc msg =
| None -> Cil.CurrentLoc.get()
| Some loc -> loc
in
- let start_pos,end_pos = loc in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file ~start_pos fmt end_pos
+ Errorloc.pp_context_from_file fmt loc
in
Kernel.abort ~current:true ~append msg
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 2ff3b6f2789fadd2b95e54ecb58cf50ca433e18e..c25b28616c1630da8af6b913405f86babc1d7b08 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -71,10 +71,10 @@ let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
let abort_context msg =
- let (start_pos,pos) = CurrentLoc.get () in
+ let loc = CurrentLoc.get () in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file ~start_pos fmt pos
+ Errorloc.pp_context_from_file fmt loc
in
Kernel.abort ~current:true ~append msg
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index 03706bd02db08d147cfbd6c353e5672083097bec..f23a21f5898553216e22419821d67dd1e2ff5c8a 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -35,7 +35,7 @@ let abort_current lex fmt =
let fmt = "before or at token %s@\n%a@\n" ^^ fmt in
Aorai_option.abort fmt
(Lexing.lexeme lex)
- (Errorloc.pp_context_from_file ~start_pos ~ctx:2) end_pos
+ (Errorloc.pp_context_from_file ~ctx:2) (start_pos,end_pos)
let unknown_token lex =
abort_current lex