From eb435af66f24a998290bc1488396f41d68b63630 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 5 Dec 2022 16:09:55 +0100
Subject: [PATCH] [printer] less invasive type pretty-printer
---
.../ast_printing/cil_printer.ml | 43 +++++++++-------
.../ast_printing/printer_api.ml | 6 +++
.../ast_printing/printer_tag.ml | 50 ++++++-------------
src/plugins/server/kernel_ast.ml | 2 +-
4 files changed, 47 insertions(+), 54 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 9e58c1b5560..afdf8712c8b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1256,8 +1256,6 @@ class cil_printer () = object (self)
| Case (e, _) -> fprintf fmt "@[%a %a:@]" self#pp_keyword "case" self#exp e
| Default _ -> fprintf fmt "@[%a:@]" self#pp_keyword "default"
- method compinfo fmt x = fprintf fmt "compinfo:%a" pp_print_bool x.cstruct
-
method builtin_logic_info fmt bli =
fprintf fmt "%a" self#varname bli.bl_name
@@ -1748,7 +1746,7 @@ class cil_printer () = object (self)
(TInt(enum.ekind,[]));
fprintf fmt "%a@[ %a {@\n%a@]@\n}%a;@\n"
self#pp_keyword "enum"
- self#varname enum.ename
+ self#enuminfo enum
(Pretty_utils.pp_list ~sep:",@\n"
(fun fmt item ->
fprintf fmt "%a = %a"
@@ -1761,17 +1759,15 @@ class cil_printer () = object (self)
self#line_directive fmt l;
fprintf fmt "%a %a;@\n"
self#pp_keyword "enum"
- self#varname enum.ename
+ self#enuminfo enum
| GCompTag (comp, l) -> (* This is a definition of a tag *)
- let n = comp.cname in
- let su = if comp.cstruct then "struct" else "union" in
let sto_mod, rest_attr = Cil.separateStorageModifiers comp.cattr in
self#line_directive ~forcefile:true fmt l;
fprintf fmt "@[<3>%a%a %a {@\n%a@]@\n}%a;@\n"
- self#pp_keyword su
+ self#compkind comp
self#attributes sto_mod
- self#varname n
+ self#compname comp
(Pretty_utils.pp_list ~sep:"@\n" self#fieldinfo)
(Option.value ~default:[] comp.cfields)
self#attributes rest_attr
@@ -1779,8 +1775,8 @@ class cil_printer () = object (self)
| GCompTagDecl (comp, l) -> (* This is a declaration of a tag *)
self#line_directive fmt l;
fprintf fmt "%a %a;@\n"
- self#pp_keyword (if comp.cstruct then "struct" else "union")
- self#varname comp.cname
+ self#compkind comp
+ self#compname comp
| GVar (vi, io, l) ->
self#line_directive ~forcefile:true fmt l;
Format.fprintf fmt "@[<hov 2>";
@@ -1942,6 +1938,21 @@ class cil_printer () = object (self)
if Cil.msvcMode () then "unsigned __int64" else "unsigned long long"
)
+ method compkind fmt ci =
+ self#pp_keyword fmt (if ci.cstruct then "struct" else "union")
+
+ method compname fmt ci =
+ self#varname fmt ci.cname
+
+ method compinfo fmt ci =
+ fprintf fmt "%a %a" self#compkind ci self#compname ci
+
+ method enuminfo fmt enum =
+ self#varname fmt enum.ename
+
+ method typeinfo fmt tinfo =
+ self#varname fmt tinfo.tname
+
method typ ?fundecl nameOpt
fmt (t:typ) =
let pname fmt space = match nameOpt with
@@ -1968,16 +1979,15 @@ class cil_printer () = object (self)
| TComp (comp, a) -> (* A reference to a struct *)
fprintf fmt
- "%a %a%a%a"
- self#pp_keyword (if comp.cstruct then "struct" else "union")
- self#varname comp.cname
+ "%a%a%a"
+ self#compinfo comp
self#attributes a
pname true
| TEnum (enum, a) ->
fprintf fmt "%a %a%a%a"
self#pp_keyword "enum"
- self#varname enum.ename
+ self#enuminfo enum
self#attributes a
pname true
@@ -2111,7 +2121,7 @@ class cil_printer () = object (self)
| TNamed (t, a) ->
fprintf fmt "%a%a%a"
- self#varname t.tname
+ self#typeinfo t
self#attributes a
pname true
@@ -2341,8 +2351,7 @@ class cil_printer () = object (self)
has 7 wide characters and the later has 3. *)
| LChr(c) -> fprintf fmt "'%s'" (Escape.escape_char c)
| LReal(r) -> fprintf fmt "%s" r.r_literal
- | LEnum {einame = s} -> self#varname fmt s
-
+ | LEnum e -> self#varname fmt e.einame
method logic_type name fmt =
let pname = match name with
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index a267b0cc6ea..c438c2a9661 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -163,6 +163,12 @@ class type extensible_printer_type = object
method ikind: Format.formatter -> ikind -> unit
method fkind: Format.formatter -> fkind -> unit
+ method compkind: Format.formatter -> compinfo -> unit
+ method compname: Format.formatter -> compinfo -> unit
+ method compinfo: Format.formatter -> compinfo -> unit
+ method enuminfo: Format.formatter -> enuminfo -> unit
+ method typeinfo: Format.formatter -> typeinfo -> unit
+
method typ:
?fundecl:varinfo ->
(Format.formatter -> unit) option -> Format.formatter -> typ -> unit
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index b1dd5a1fa8c..3718f384dd3 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -814,42 +814,20 @@ struct
let tag = Tag.create (PStmtStart(f,s)) in
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 ->
- 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
+ method! compname fmt comp =
+ Format.fprintf fmt "@{<%s>%a}"
+ (Tag.create (PType (TComp (comp, []))))
+ super#compname comp
+
+ method! enuminfo fmt enum =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PType (TEnum (enum, []))))
+ super#enuminfo enum
+
+ method! typeinfo fmt tinfo =
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Tag.create (PType (TNamed (tinfo, []))))
+ super#typeinfo tinfo
initializer force_brace <- true
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 53ccbf8fa2a..f24c0839196 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -723,7 +723,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.typesizeof"
~label:"Sizeof"
- ~title:"Size of a C type"
+ ~descr:"Size of a C type"
begin fun fmt loc ->
match loc with
| PType typ -> Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
--
GitLab