diff --git a/src/kernel_services/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml index 39e7f83db2562220bacb41352c737e1d108369ec..e250732f252f426783e6c11e79f1b1dca2519e46 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 3533691b55f7a5a731cd1fc42f4ac255547d7a8e..23fae8af0b0a01e91e26e9176739a33f5f7de4d2 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 888fe0d6ff3ef9710e4f01768bde4ace9072c20f..20d23f66547df8d412b198e4b737c56db12106f9 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