From f692ccac895534fb34e8e2e90ff477e85303c455 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 Jul 2024 18:18:16 +0200
Subject: [PATCH] [cil/utils] type & size of array types
---
src/kernel_services/ast_queries/cil.ml | 9 ++++++---
src/kernel_services/ast_queries/cil.mli | 6 ++++++
2 files changed, 12 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 132d30d68c5..dd9c80abda0 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 cb016440a6c..e5a54e543c6 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 *)
--
GitLab