From 3a305fdd9c8168713086dbffed665d8d80150f4d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 17 Feb 2022 17:23:10 +0100
Subject: [PATCH] [kernel] add Cil.visitCilFileFunction to only visit function
definitions
Keep the APIs of Visitor and Cil.visit* in sync
---
src/kernel_services/analysis/undefined_sequence.ml | 7 +------
src/kernel_services/ast_queries/cil.ml | 7 +++++++
src/kernel_services/ast_queries/cil.mli | 6 ++++++
3 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml
index 39e7f83db25..e250732f252 100644
--- a/src/kernel_services/analysis/undefined_sequence.ml
+++ b/src/kernel_services/analysis/undefined_sequence.ml
@@ -144,11 +144,6 @@ let check_sequences file =
| _ -> ());
Cil.DoChildren
- (* Optimization: only visits function definitions. *)
- method! vglob = function
- | GFun _ -> Cil.DoChildren
- | _ -> Cil.SkipChildren
-
method! vinst _ = SkipChildren
method! vexpr _ = SkipChildren
method! vlval _ = SkipChildren
@@ -157,4 +152,4 @@ let check_sequences file =
method! vcode_annot _ = SkipChildren
end
in
- Cil.visitCilFileSameGlobals check_unspec file
+ Cil.visitCilFileFunctions check_unspec file
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 3533691b55f..23fae8af0b0 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5365,6 +5365,13 @@ let visitCilFileSameGlobals (vis : cilVisitor) (f : file) : unit =
ignore
(doVisitCil vis (Visitor_behavior.cfile vis#behavior) (post_file vis) childrenFileSameGlobals f)
+let visitCilFileFunctions vis file =
+ let process_one_global = function
+ | GFun (fundec, _) -> ignore (visitCilFunction vis fundec)
+ | _ -> ()
+ in
+ iterGlobals file process_one_global
+
let childrenFileCopy vis f =
let fGlob g = visitCilGlobal vis g in
(* Scan the globals. Make sure this is tail recursive. *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 888fe0d6ff3..20d23f66547 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1880,6 +1880,12 @@ val visitCilFile: cilVisitor -> file -> unit
@plugin development guide *)
val visitCilFileSameGlobals: cilVisitor -> file -> unit
+(** Same as {!visitCilFilesSameGlobals}, but only visits function definitions
+ (i.e. behaves as if all globals but [GFun] return [SkipChildren]).
+ @since Frama-C+dev
+*)
+val visitCilFileFunctions: cilVisitor -> file -> unit
+
(** Visit a global *)
val visitCilGlobal: cilVisitor -> global -> global list
--
GitLab