From 0c5d3963f49f010df71492e7fb8e4bff9993a7be Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 15 Feb 2023 19:06:04 +0100
Subject: [PATCH] [Kernel] Ast_info: add function get_statics (previously at
 Kernel_function)

---
 src/kernel_services/ast_data/kernel_function.ml | 12 +-----------
 src/kernel_services/ast_queries/ast_info.ml     | 16 ++++++++++++++++
 src/kernel_services/ast_queries/ast_info.mli    |  4 ++++
 3 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index fd461ee5e9b..64b0286d4a8 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -54,17 +54,7 @@ let get_locals f = match f.fundec with
 
 let get_statics f = match f.fundec with
   | Definition (d, _) ->
-    let statics = ref [] in
-    let local_statics_visitor =
-      object
-        inherit Cil.nopCilVisitor
-        method! vblock b =
-          statics := !statics @ b.bstatics;
-          Cil.DoChildren
-      end
-    in
-    ignore (Cil.visitCilBlock local_statics_visitor d.sbody);
-    !statics
+    Ast_info.Function.get_statics d
   | Declaration (_, _, _, _) -> []
 
 let () = Globals.get_statics := get_statics
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 2c9418a9254..e1c019546c4 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -364,6 +364,22 @@ module Function = struct
   let get_name f = (get_vi f).vname
   let get_id f = (get_vi f).vid
 
+  let get_statics fundec =
+    let statics = ref [] in
+    let local_statics_visitor =
+      object
+        inherit Cil.nopCilVisitor
+        method! vblock b =
+          statics := !statics @ b.bstatics;
+          Cil.DoChildren
+        method! vinst _ = Cil.SkipChildren
+        method! vvdec _ = Cil.SkipChildren
+        method! vexpr _ = Cil.SkipChildren
+      end
+    in
+    ignore (Cil.visitCilBlock local_statics_visitor fundec.sbody);
+    !statics
+
 end
 
 exception FoundBlock of block
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 36fefd01687..b068cb7fac8 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -230,6 +230,10 @@ module Function: sig
   val get_vi: cil_function -> varinfo
   val get_name: cil_function -> string
   val get_id: cil_function -> int
+
+  val get_statics: fundec -> varinfo list
+  (** @since Frama-C+dev *)
+
 end
 
 (* ************************************************************************** *)
-- 
GitLab