diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 41e7fc764fb4eef1191161a2295b969ab7b5740d..873e9e181d0b5ee8b5e7dec812009c48fdfcc3ea 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -766,7 +766,10 @@ let () = Information.register | PGlobal (GEnumTagDecl(ei,_) | GEnumTag(ei,_)) -> TEnum(ei,[]) | _ -> raise Not_found in - let bits = Cil.bitsSizeOf typ in + let bits = + try Cil.bitsSizeOf typ + with Cil.SizeOfError _ -> raise Not_found + in let bytes = bits / 8 in let rbits = bits mod 8 in if rbits > 0 then