diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml index ee6d4ef5573f305005e6e8ca321218f73bf56986..ef12ae7e9f1918b0e6d6f610be9b26642b78176d 100644 --- a/src/kernel_services/ast_queries/cil_datatype.ml +++ b/src/kernel_services/ast_queries/cil_datatype.ml @@ -206,6 +206,10 @@ module Position = struct let pp_with_col fmt pos = Format.fprintf fmt "%a char %d" pretty pos (pos.Filepath.pos_cnum - pos.Filepath.pos_bol) + let pretty_debug fmt pos = + Format.fprintf fmt "%a:%d:%d" + Datatype.Filepath.pretty pos.Filepath.pos_path + pos.Filepath.pos_lnum pos.Filepath.pos_cnum end module Location = struct @@ -242,11 +246,8 @@ module Location = struct Format.fprintf fmt "generated" let pretty_debug fmt loc = - Format.fprintf fmt "(%a:%d:%d,%a:%d:%d)" - Datatype.Filepath.pretty (fst loc).Filepath.pos_path - (fst loc).Filepath.pos_lnum (fst loc).Filepath.pos_cnum - Datatype.Filepath.pretty (snd loc).Filepath.pos_path - (snd loc).Filepath.pos_lnum (snd loc).Filepath.pos_cnum + Format.fprintf fmt "(%a,%a)" + Position.pretty_debug (fst loc) Position.pretty_debug (snd loc) let of_lexing_loc (pos1, pos2) = Position.of_lexing_pos pos1, Position.of_lexing_pos pos2 diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli index df5138305b7a051784a19e7f9c6e893383ac0648..f1064f288f97e0a6192087f5def008d9a4ea80ca 100644 --- a/src/kernel_services/ast_queries/cil_datatype.mli +++ b/src/kernel_services/ast_queries/cil_datatype.mli @@ -58,6 +58,11 @@ module Position: sig val pp_with_col : Format.formatter -> t -> unit val of_lexing_pos : Lexing.position -> t val to_lexing_pos : t -> Lexing.position + + (** Pretty-print file, line and character offset. + @since Frama-C+dev + *) + val pretty_debug: t Pretty_utils.formatter end (** Cil locations. *)