From b93824e6314298ea25e04e3db6331f4a6873a48b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 4 Feb 2022 21:21:42 +0100
Subject: [PATCH] [Cil] add debug pretty-printer for position
---
src/kernel_services/ast_queries/cil_datatype.ml | 11 ++++++-----
src/kernel_services/ast_queries/cil_datatype.mli | 5 +++++
2 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index ee6d4ef5573..ef12ae7e9f1 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 df5138305b7..f1064f288f9 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. *)
--
GitLab