From 89c4ee50fb85ee78f7cbacc3c7ec12b78d6e3dd6 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 8 Apr 2022 18:49:07 +0200
Subject: [PATCH] [kernel] Printer_tag add tags only to direct types
---
.../ast_printing/printer_tag.ml | 35 +++++++++++++++++--
1 file changed, 32 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index a41a627b014..b1dd5a1fa8c 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -815,12 +815,41 @@ struct
Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
method! typ ?fundecl fmt_opt fmt typ =
+ (* Extracted from Cil_printer *)
+ let pname fmt space = match fmt_opt with
+ | None -> ()
+ | Some d -> Format.fprintf fmt "%s%t" (if space then " " else "") d
+ in
match fundecl with
| Some _ -> super#typ ?fundecl fmt_opt fmt typ
| None ->
- Format.fprintf fmt "@{<%s>%a@}"
- (Tag.create (PType typ))
- (super#typ ?fundecl fmt_opt) typ
+ match typ with
+ | TNamed (t, a) ->
+ Format.fprintf fmt "@{<%s>%a@}%a%a"
+ (Tag.create (PType (TNamed (t, []))))
+ self#varname t.tname
+ self#attributes a
+ pname true
+
+ | TComp (comp, a) ->
+ Format.fprintf fmt
+ "@{<%s>%a %a@}%a%a"
+ (Tag.create (PType (TComp (comp, []))))
+ self#pp_keyword (if comp.cstruct then "struct" else "union")
+ self#varname comp.cname
+ self#attributes a
+ pname true
+
+ | TEnum (enum, a) ->
+ Format.fprintf fmt "@{<%s>%a %a@}%a%a"
+ (Tag.create (PType (TEnum (enum, []))))
+ self#pp_keyword "enum"
+ self#varname enum.ename
+ self#attributes a
+ pname true
+
+ | _ ->
+ super#typ ?fundecl fmt_opt fmt typ
initializer force_brace <- true
--
GitLab