From 13a4a4da0a6cd0082a00e77b275b579a028944dd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 6 Mar 2023 09:45:34 +0100
Subject: [PATCH] [printer] fix pp-print-head api
---
src/kernel_services/ast_printing/cil_printer.ml | 8 ++++----
src/kernel_services/ast_printing/printer_api.ml | 10 +++++-----
src/kernel_services/ast_printing/printer_tag.ml | 4 ++--
3 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c96a5e1b00a..cd8d3806d7e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1442,15 +1442,15 @@ class cil_printer () = object (self)
directive (fst l).Filepath.pos_lnum filename
(* Print a recovered while condition from Loop *)
- method pp_while fmt cond =
+ method pp_while_head fmt cond =
fprintf fmt "%a (%a)"
self#pp_keyword "while"
self#exp cond
- method private stacked_while ~stmt ~cond fmt =
+ method private pp_while_head_stacked ~stmt ~cond fmt =
begin
Stack.push stmt current_stmt;
- self#pp_while fmt cond;
+ self#pp_while_head fmt cond;
ignore (Stack.pop current_stmt);
end
@@ -1642,7 +1642,7 @@ class cil_printer () = object (self)
in
Format.fprintf fmt "%a@[<v 2>%t %t%a@]"
(fun fmt -> self#line_directive fmt) l
- (self#stacked_while ~stmt ~cond)
+ (self#pp_while_head_stacked ~stmt ~cond)
pp_sattr
(self#unboxed_block Other) b;
with Not_found ->
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index f9236745782..230e0bce02e 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -312,11 +312,11 @@ class type extensible_printer_type = object
(** {3 Modifying pretty-printer behavior} *)
(* ******************************************************************* *)
- method pp_while: Format.formatter -> exp -> unit
- (** Prints the recovered [while (cond)] exit condition of a loop. The current
- stmt is expected to be positionned to the original AST statement
- containing the breaking condition (which is not printed at all). *)
-
+ method pp_while_head: Format.formatter -> exp -> unit
+ (** Prints the recovered [while (cond)] exit condition of a loop. Note: this
+ method will be called in a context where 'current_stmt' is tied to the
+ original AST conditional statement that exits the loop, as expected. *)
+
method pp_keyword: Format.formatter -> string -> unit
(** All C99 keywords except types "char", "int", "long", "signed",
"short", "unsigned", "void" and "_XXX" (like "_Bool") **)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index f392f73483f..867ccc77835 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -582,12 +582,12 @@ struct
pp_by_kf fmt ips_all_kfs
| _ -> ()
- method! pp_while fmt cond =
+ method! pp_while_head fmt cond =
let kf = Option.get self#current_kf in
let stmt = Option.get self#current_stmt in
Format.fprintf fmt "@{<%s>%a@}"
(Tag.create (PStmtStart(kf,stmt)))
- super#pp_while cond
+ super#pp_while_head cond
method! next_stmt next fmt current =
if Tag.unfold current
--
GitLab