From 27554b52887c75ef2d59eb611c265a254b4086b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 18 Jun 2024 13:36:41 +0200
Subject: [PATCH] [cil] getCompField
---
src/kernel_services/ast_queries/cil.ml | 5 +++++
src/kernel_services/ast_queries/cil.mli | 2 ++
2 files changed, 7 insertions(+)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fd438e7de13..24d8d26e36f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5936,6 +5936,11 @@ let getCompField cinfo fieldName =
(fun fi -> fi.fname = fieldName)
(Option.value ~default:[] cinfo.cfields)
+let getCompType typ =
+ match unrollTypeSkel typ with
+ | TComp(comp,_) -> comp
+ | _ -> raise Not_found
+
let sameSizeInt ?(machdep=false) (ik1 : ikind) (ik2 : ikind) =
if machdep then bytesSizeOfInt ik1 == bytesSizeOfInt ik2
else
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2e07fd68287..83a9b53210a 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -658,6 +658,8 @@ val lenOfArray64: exp option -> Integer.t
(** Return a named fieldinfo in compinfo, or raise Not_found *)
val getCompField: compinfo -> string -> fieldinfo
+(** Return the compinfo of the typ, or raise Not_found *)
+val getCompType: typ -> compinfo
(** A datatype to be used in conjunction with [existsType] *)
type existsAction =
--
GitLab