[AST Printing] Exposes (private) in_ghost_if_needed in printer_api

src/kernel_services/ast_printing/printer.ml

@@ -189,20 +189,6 @@ class printer_with_annot () = object (self)
       fmt
       annots
 
-  method private in_ghost_if_needed fmt ghost_flag do_it =
-    let display_ghost = ghost_flag && not is_ghost in
-    if display_ghost then begin
-      is_ghost <- true ;
-      Format.fprintf fmt "@[%t %a@ "
-        (fun fmt -> self#pp_open_annotation fmt)
-        self#pp_acsl_keyword "ghost"
-    end ;
-    do_it () ;
-    if display_ghost then begin
-      is_ghost <- false;
-      Format.fprintf fmt "%t@]" (fun fmt -> self#pp_close_annotation fmt)
-    end
-
   method! annotated_stmt next fmt s =
     (* To debug location setting:
        (let loc = fst (Cil_datatype.Stmt.loc s.skind) in
@@ -227,7 +213,7 @@ class printer_with_annot () = object (self)
           Cil_datatype.Code_annotation.compare
           (Annotations.code_annot s)
       in
-      self#in_ghost_if_needed fmt s.ghost
+      self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
         (fun () -> match all_annot with
            | [] ->  self#stmtkind s.sattr next fmt s.skind;
            | [ a ] when Cil.is_skip s.skind && not s.ghost ->

src/kernel_services/ast_printing/printer_api.mli

@@ -78,6 +78,22 @@ class type extensible_printer_type = object
   method private has_annot: bool
   (** [true] if [current_stmt] has some annotations attached to it. *)
 
+  method private in_ghost_if_needed:
+    Format.formatter ->
+    bool ->
+    post_fmt:(((Format.formatter -> unit) -> unit, Format.formatter, unit) format) ->
+    ?block:bool ->
+    (unit -> unit)
+    -> unit
+  (** Open a ghost context if the the first [bool] is true and we are not already
+      in a ghost context. [post_fmt] is a format like ["%t"] and is used to define
+      the format of the end of the ghost context. [block] indicates whether we
+      should open a C block or not (and defaults to [true]). The last parameter is
+      the function to perform in the ghost context (generally some AST element).
+
+      @since 19.0-Potassium+dev
+  *)
+
   method private current_stmt: stmt option
   (** @return the [stmt] being printed *)