diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 4359de2e4410742d3e0a1e45315eb7ca8d8779c5..b77c6c0e7fe196d03d4e47f3a515369d58d71d76 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 (* -------------------------------------------------------------------------- *)