diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml index 6a86f2b90e6df109d5763141221e84929f1b65fb..0151681546e289610e4244aca60313054a9d30a5 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/src/plugins/e-acsl/typing.ml @@ -226,7 +226,7 @@ let type_constant ty = function | LStr _ | LWStr _ | LReal _ | LEnum _ -> No_integral ty let size_of ty = - try int_to_interv (Cil.sizeOf_int ty) + try int_to_interv (Cil.bytesSizeOf ty) with Cil.SizeOfError _ -> eacsl_typ_of_typ Cil.ulongLongType let align_of ty = int_to_interv (Cil.bytesAlignOf ty)