From 012cf6f1375fe7fe4d94cd46e813491a5e48e479 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 24 Nov 2023 14:55:08 +0100 Subject: [PATCH] [server] simplifies typedefs for type markers --- src/plugins/server/kernel_ast.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index b0954e3174e..8a0936ec6f4 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -843,11 +843,9 @@ let () = Information.register ~title:"Type Definition" begin fun fmt loc -> match loc with - | PGlobal - (( GType _ - | GCompTag _ | GCompTagDecl _ - | GEnumTag _ | GEnumTagDecl _ - ) as g) -> Printer.pp_global fmt g + | PType (TNamed _ as ty) + | PGlobal (GType({ ttype = ty },_)) -> + Printer.pp_typ fmt (Cil.unrollType ty) | _ -> raise Not_found end -- GitLab