From cdc940d567155eb49c7d6828e428326a84cce5b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 2 Mar 2023 15:35:26 +0100
Subject: [PATCH] [printer] clarify StmtStart
---
src/kernel_services/ast_printing/printer_tag.ml | 2 +-
src/kernel_services/ast_printing/printer_tag.mli | 9 +++++++--
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 6684aa01fc5..e73b16d8b08 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -584,7 +584,7 @@ struct
method! pp_while ~stmt ~cond fmt =
Format.fprintf fmt "@{<%s>%t@}"
- (Tag.create (PStmt(Option.get self#current_kf,stmt)))
+ (Tag.create (PStmtStart(Option.get self#current_kf,stmt)))
(super#pp_while ~stmt ~cond)
method! next_stmt next fmt current =
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index 57de33aaba6..d30adb07b61 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -27,18 +27,23 @@ open Cil_types
(** The kind of object that can be selected in the source viewer. *)
type localizable =
| PStmt of (kernel_function * stmt)
+ (** Full statement (with attributes, annotations, etc.) *)
| PStmtStart of (kernel_function * stmt)
+ (** Naked statement (only skind, without attributes, annotations, etc.) *)
| PLval of (kernel_function option * kinstr * lval)
+ (** L-Values *)
| PExp of (kernel_function option * kinstr * exp)
+ (** Non l-value expressions *)
| PTermLval of (kernel_function option * kinstr * Property.t * term_lval)
+ (** Term l-values inside properties *)
| PVDecl of (kernel_function option * kinstr * varinfo)
(** Declaration and definition of variables and function. Check the type
of the varinfo to distinguish between the various possibilities.
If the varinfo is a global or a local, the kernel_function is the
one in which the variable is declared. The [kinstr] argument is given
for local variables with an explicit initializer. *)
- | PGlobal of global (** all globals but variable declarations and function
- definitions. *)
+ | PGlobal of global
+ (** Global definitions except global variables and functions. *)
| PIP of Property.t
| PType of typ
--
GitLab