From 5c9e99e515d238a9420b86c7eb80c002d32afdb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 13 Dec 2022 15:06:32 +0100
Subject: [PATCH] [ivette] inspector all types sizeof in bytes
---
src/plugins/server/kernel_ast.ml | 16 +++++++++++++---
1 file changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 4359de2e441..b77c6c0e7fe 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -761,10 +761,20 @@ let () = Information.register
match loc with
| PType typ -> typ
| PGlobal (GType(ti,_)) -> ti.ttype
- | PGlobal (GCompTagDecl(ci,_)) -> TComp(ci,[])
- | PGlobal (GEnumTagDecl(ei,_)) -> TEnum(ei,[])
+ | PGlobal (GCompTagDecl(ci,_) | GCompTag(ci,_)) -> TComp(ci,[])
+ | PGlobal (GEnumTagDecl(ei,_) | GEnumTag(ei,_)) -> TEnum(ei,[])
| _ -> raise Not_found
- in Format.fprintf fmt "%i bits" (Cil.bitsSizeOf typ)
+ in
+ let bits = Cil.bitsSizeOf typ in
+ let bytes = bits / 8 in
+ let rbits = bits mod 8 in
+ if rbits > 0 then
+ if bytes > 0 then
+ Format.fprintf fmt "%d bytes + %d bits" bytes rbits
+ else
+ Format.fprintf fmt "%d bits" rbits
+ else
+ Format.fprintf fmt "%d bytes" bytes
end
(* -------------------------------------------------------------------------- *)
--
GitLab