diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 132d30d68c5e67a30f5ee892952e95ba6a38a3c0..dd9c80abda0b4c0838a65ba493617444d1d296c9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3635,19 +3635,22 @@ let setReturnTypeVI (v: varinfo) (t: typ) =
 let setReturnType (f:fundec) (t:typ) =
   setReturnTypeVI f.svar t
 
-(** Returns the type pointed by the given type. Asserts it is a pointer type *)
 let typeOf_pointed typ =
   match unrollType typ with
   | TPtr (typ,_) -> typ
   | _ -> Kernel.fatal "Not a pointer type %a" !pp_typ_ref typ
 
-(** Returns the type of the elements of the array. Asserts it is an array type
-*)
 let typeOf_array_elem t =
   match unrollType t with
   | TArray (ty_elem, _, _) -> ty_elem
   | _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
 
+let typeOf_array_elem_size t =
+  match unrollType t with
+  | TArray (ty_elem, arr_size, _ ) ->
+    ty_elem, Option.bind arr_size !constfoldtoint
+  | _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
+
 let no_op_coerce typ t =
   match typ with
   | Lreal -> isLogicArithmeticType t.term_type
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index cb016440a6ce183d18b3732dd68c6bbf700b15ec..e5a54e543c600d0ba69656229aa16b3632b7e56d 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1253,6 +1253,12 @@ val typeOf_array_elem : typ -> typ
 (** Returns the type of the array elements of the given type.
     Asserts it is an array type. *)
 
+val typeOf_array_elem_size : typ -> typ * Z.t option
+(** Returns the type of the array elements of the given type, and the size
+    of the array, if any.
+    Asserts it is an array type.
+    @since Frama-C+dev *)
+
 val is_fully_arithmetic: typ -> bool
 (** Returns [true] whenever the type contains only arithmetic types *)