diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 33db76d4d32bdabcaff5b6f8ebef05a95980e1ae..765167a4084cecb31a45fe78a86076d1c05c242b 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -245,13 +245,13 @@ export const markerInfo: State.Array<string,markerInfoData> = markerInfo_interna
 export type marker =
   Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
   Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
-  Json.key<'#property'>;
+  Json.key<'#property'> | Json.key<'#type'>;
 
 /** Decoder for `marker` */
 export const jMarker: Json.Decoder<marker> =
   Json.jUnion<Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
               Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
-              Json.key<'#property'>>(
+              Json.key<'#property'> | Json.key<'#type'>>(
     Json.jKey<'#stmt'>('#stmt'),
     Json.jKey<'#decl'>('#decl'),
     Json.jKey<'#lval'>('#lval'),
@@ -259,6 +259,7 @@ export const jMarker: Json.Decoder<marker> =
     Json.jKey<'#term'>('#term'),
     Json.jKey<'#global'>('#global'),
     Json.jKey<'#property'>('#property'),
+    Json.jKey<'#type'>('#type'),
   );
 
 /** Natural order for `marker` */
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index afdf8712c8be2825e07eec83c23c1943fc6ebbb4..a7ab50d30010d65852dc2b63977a1ee051a7f7e6 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1777,6 +1777,7 @@ class cil_printer () = object (self)
         fprintf fmt "%a %a;@\n"
           self#compkind comp
           self#compname comp
+
       | GVar (vi, io, l) ->
         self#line_directive ~forcefile:true fmt l;
         Format.fprintf fmt "@[<hov 2>";
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 3718f384dd351b673651549d4590ab9748a2e39c..b9f386abb97e04db388b79d1ce8c6d65a85bdaff 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -40,8 +40,12 @@ type localizable =
 
 let glabel = function
   | GType(tinfo,_) -> tinfo.tname
-  | GCompTag(comp, _) | GCompTagDecl(comp, _) -> comp.cname
-  | GEnumTag(enum, _) | GEnumTagDecl(enum, _) -> enum.ename
+  | GCompTag(comp, _) | GCompTagDecl(comp, _) ->
+    Printf.sprintf "%s %s"
+      (if comp.cstruct then "struct" else "union")
+      comp.cname
+  | GEnumTag(enum, _) | GEnumTagDecl(enum, _) ->
+    Printf.sprintf "enum %s" enum.ename
   | GVarDecl(vi,_) | GVar(vi, _, _)
   | GFun( { svar=vi }, _) | GFunDecl(_,vi,_) -> vi.vname
   | GPragma((Attr(a,_) | AttrAnnot a),_) -> a
@@ -58,7 +62,7 @@ let label = function
   | PTermLval _ -> "(term)"
   | PGlobal g -> glabel g
   | PIP _ -> "(property)"
-  | PType _ -> "(type)"
+  | PType ty -> Pretty_utils.to_string Printer.pp_typ ty
 
 let decl_of = function
   | GCompTag(comp,loc) -> GCompTagDecl(comp,loc)
@@ -676,13 +680,14 @@ struct
 
     method! global fmt g =
       match g with
-      (* these globals are already covered by PVDecl *)
-      | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ -> super#global fmt g
-      | _ ->
-        Format.fprintf fmt "@{<%s>%a@}"
-          (Tag.create (PGlobal g))
-          super#global
-          g
+      (* these globals are already covered by the underlying parser *)
+      | GVarDecl _ | GVar _ | GFunDecl _ | GFun _
+      | GCompTag _ | GCompTagDecl _
+      | GEnumTag _ | GEnumTagDecl _
+      | GType _ ->
+        super#global fmt g
+      | GAsm _ | GPragma _ | GText _ | GAnnot _ ->
+        Format.fprintf fmt "@{<%s>%a@}" (Tag.create (PGlobal g)) super#global g
 
     method! extended fmt ext =
       let loc =
@@ -814,19 +819,29 @@ struct
       let tag = Tag.create (PStmtStart(f,s)) in
       Format.fprintf fmt "@{<%s>%a@}" tag (super#stmtkind sattr next) sk
 
+    method! ikind fmt c =
+      Format.fprintf fmt "@{<%s>%a@}"
+        (Tag.create (PType(TInt(c,[]))))
+        super#ikind c
+
+    method! fkind fmt c =
+      Format.fprintf fmt "@{<%s>%a@}"
+        (Tag.create (PType(TFloat(c,[]))))
+        super#fkind c
+
     method! compname fmt comp =
-      Format.fprintf fmt "@{<%s>%a}"
-        (Tag.create (PType (TComp (comp, []))))
+      Format.fprintf fmt "@{<%s>%a@}"
+        (Tag.create (PGlobal(Globals.Types.global Struct comp.cname)))
         super#compname comp
 
     method! enuminfo fmt enum =
       Format.fprintf fmt "@{<%s>%a@}"
-        (Tag.create (PType (TEnum (enum, []))))
+        (Tag.create (PGlobal(Globals.Types.global Enum enum.ename)))
         super#enuminfo enum
 
     method! typeinfo fmt tinfo =
       Format.fprintf fmt "@{<%s>%a@}"
-        (Tag.create (PType (TNamed (tinfo, []))))
+        (Tag.create (PGlobal(Globals.Types.global Typedef tinfo.tname)))
         super#typeinfo tinfo
 
     initializer force_brace <- true
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 170fafd311e01dc50746682853edb952ad3b45bb..e314f33f7c59ff03dd5a5dd4bf442ded0da30932 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -730,12 +730,16 @@ let () = Information.register
     ~label:"Sizeof"
     ~descr:"Size of a C type"
     begin fun fmt loc ->
-      match loc with
-      | PType typ -> Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
-      | _ -> raise Not_found
+      let typ =
+        match loc with
+        | PType typ -> typ
+        | PGlobal (GType(ti,_)) -> ti.ttype
+        | PGlobal (GCompTagDecl(ci,_)) -> TComp(ci,[])
+        | PGlobal (GEnumTagDecl(ei,_)) -> TEnum(ei,[])
+        | _ -> raise Not_found
+      in Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
     end
 
-
 (* -------------------------------------------------------------------------- *)
 (* --- Marker at a position                                               --- *)
 (* -------------------------------------------------------------------------- *)