[kernel] Visitor: adds a function to visit all function definitions of a file.

For visitors that only need function C bodies, replaces uses of
[visitFramacFileSameGlobals], which visits all globals of a file, by
[visitFramacFileFunctions], which visits only function definitions.

Also optimizes these visitors by skipping the visit of some nodes,
especially the visit of functions specifications and code annotations.

src/kernel_internals/typing/allocates.ml

@@ -57,11 +57,15 @@ class vis_add_loop_allocates =
       );
       Cil.DoChildren
 
-    method! vinst _ = Cil.SkipChildren
-
+    method! vinst _ = SkipChildren
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
 
 let add_allocates_nothing () =
   Globals.Functions.iter add_allocates_nothing_funspec;
   let vis = new vis_add_loop_allocates in
-  Visitor.visitFramacFileSameGlobals vis (Ast.get ())
+  Visitor.visitFramacFileFunctions vis (Ast.get ())

src/kernel_internals/typing/asm_contracts.ml

@@ -221,11 +221,17 @@ class visit_assembly =
           ~dkey:Kernel.dkey_asm_contracts "Ignoring basic assembly instruction";
         Cil.SkipChildren
       | _ -> Cil.SkipChildren
+
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
 
 let transform file =
   if Kernel.AsmContractsGenerate.get() then
-    Visitor.visitFramacFileSameGlobals (new visit_assembly) file
+    Visitor.visitFramacFileFunctions (new visit_assembly) file
 
 let () =
   File.add_code_transformation_after_cleanup

src/kernel_internals/typing/unroll_loops.ml

@@ -709,6 +709,13 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
       ChangeDoChildrenPost (s, fgh)
 
     | _ -> DoChildren
+
+  method! vinst _ = SkipChildren
+  method! vexpr _ = SkipChildren
+  method! vlval _ = SkipChildren
+  method! vtype _ = SkipChildren
+  method! vspec _ = SkipChildren
+  method! vcode_annot _ = SkipChildren
 end
 
 (* Performs unrolling transformation without using -ulevel option.
@@ -723,7 +730,7 @@ let apply_transformation ?(force=true) nb file =
     in
     let visitor = new do_it global_find_init (force, nb) in
     Kernel.debug ~dkey "Using -ulevel %d option and UNROLL loop pragmas@." nb;
-    visitFramacFileSameGlobals (visitor:>Visitor.frama_c_visitor) file;
+    visitFramacFileFunctions (visitor:>Visitor.frama_c_visitor) file;
     if !ast_has_changed then Ast.mark_as_changed ()
     else begin
       Kernel.debug ~dkey

src/kernel_services/analysis/exn_flow.ml

@@ -65,11 +65,17 @@ class all_exn =
         all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
         SkipChildren
       | _ -> DoChildren
+    method! vinst _ = SkipChildren
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
 
 let compute_all_exn () =
   let vis = new all_exn in
-  Visitor.visitFramacFileSameGlobals (vis:>Visitor.frama_c_visitor) (Ast.get());
+  Visitor.visitFramacFileFunctions (vis:>Visitor.frama_c_visitor) (Ast.get());
   vis#get_exn
 
 let all_exn () = All_exn.memo compute_all_exn
@@ -259,6 +265,11 @@ class exn_visit =
       in
       DoChildrenPost after_visit
 
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
 
 let compute_kf kf =
@@ -857,7 +868,7 @@ let prepare_file f =
 
 let remove_exn f =
   if Kernel.RemoveExn.get() then begin
-    Visitor.visitFramacFileSameGlobals (new exn_visit) f;
+    Visitor.visitFramacFileFunctions (new exn_visit) f;
     let vis = new erase_exn in
     Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) f;
     let funs = vis#modified_funcs in

src/kernel_services/ast_transformations/inline.ml

@@ -342,6 +342,11 @@ let inliner functions_to_inline = object (self)
          let kf = Globals.Functions.get f.svar in
          already_visited <- Cil_datatype.Kf.Set.add kf functions_to_inline; f)
 
+  method! vexpr _ = SkipChildren
+  method! vlval _ = SkipChildren
+  method! vtype _ = SkipChildren
+  method! vspec _ = SkipChildren
+  method! vcode_annot _ = SkipChildren
 end
 
 let remove_local_statics = object
@@ -379,7 +384,7 @@ end
 let inline_calls ast =
   if not (InlineCalls.is_empty ()) then begin
     let functions = InlineCalls.get() in
-    Visitor.visitFramacFileSameGlobals (inliner functions) ast;
+    Visitor.visitFramacFileFunctions (inliner functions) ast;
     Cil_datatype.Kf.Set.iter
       (fun kf -> ignore (Visitor.visitFramacKf remove_local_statics kf))
       functions;

src/kernel_services/visitors/visitor.ml

@@ -871,6 +871,13 @@ let visitFramacFunction vis f =
   Option.iter vis#set_current_kf old_current_kf;
   vis#fill_global_tables; f'
 
+let visitFramacFileFunctions vis file =
+  let process_one_global = function
+    | GFun (fundec, _) -> ignore (visitFramacFunction vis fundec)
+    | _ -> ()
+  in
+  Cil.iterGlobals file process_one_global
+
 let visitFramacKf vis kf =
   let glob = Ast.def_or_last_decl (Kernel_function.get_vi kf) in
   ignore (visitFramacGlobal vis glob);

src/kernel_services/visitors/visitor.mli

@@ -115,6 +115,13 @@ val visitFramacFile: frama_c_visitor -> file -> unit
     @plugin development guide *)
 val visitFramacFileSameGlobals: frama_c_visitor -> file -> unit
 
+(** Visit all function definitions of a file. Use this function instead of
+    {!Visitor.visitFramacFile} or {!Visitor.visitFramacFileSameGlobals} if your
+    visitor only needs function bodies to avoid visiting other globals,
+    including libc functions and their specifications.
+    @since Frama-c+dev *)
+val visitFramacFileFunctions: frama_c_visitor -> file -> unit
+
 (** Visit a global.
 
     {b Warning} Do not call this function during another visit using the

src/plugins/value/legacy/eval_annots.ml

@@ -96,11 +96,16 @@ let mark_unreachable () =
       end;
       Cil.DoChildren
 
-    method! vinst _ = Cil.SkipChildren
+    method! vinst _ = SkipChildren
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
   in
   Annotations.iter_all_code_annot do_code_annot;
-  Visitor.visitFramacFile unreach (Ast.get ())
+  Visitor.visitFramacFileFunctions unreach (Ast.get ())
 
 let c_labels kf cs =
   if !Db.Value.use_spec_instead_of_definition kf then

src/plugins/value/partitioning/split_return.ml

@@ -208,6 +208,10 @@ module ReturnUsage = struct
 
     method result () =
       summarize_by_lv usage
+
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
 
   (* For functions returning pointers, add a split on NULL/non-NULL *)
@@ -223,7 +227,7 @@ module ReturnUsage = struct
 
   let compute file =
     let vis = new visitorVarUsage in
-    Visitor.visitFramacFileSameGlobals (vis:> Visitor.frama_c_visitor) file;
+    Visitor.visitFramacFileFunctions (vis:> Visitor.frama_c_visitor) file;
     let split_compared = vis#result () in
     let split_null_pointers = add_null_pointers_split split_compared in
     split_null_pointers