diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index dec3566fe2166838fc785c3911aaa83368fc63fa..92f755e9cbb8dc2b21b8db773452a87843dc3ca5 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/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 ())
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 55c5b0fb1f41fe6fed44bfce1bd690bf9cc2f982..c2c8e143093ccc647f9fa19fb66ae49c2e5750c7 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/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
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 89c96fbb3a542cb595dd29918779d84587c6ce5e..1242f533128cc6c521a523467e2cf1cf70eb54a3 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/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
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index f6dd804a26cad36fb2dad70cca71704f0d137671..ad3a19d463a1bdee7e38247a2975a7220c3b4449 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/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
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index b8cddec6cc6684e6e760fab6b3bd58a6073618ad..8e3d83b946f58048f5b87980457603c767d281fb 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/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;
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 1121a89660db3dbbbd7bdc5dd362fe2a866903b2..fdb824e963c3fbcddc7d9b570f24155ea3e52483 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/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);
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 8b0a5da0742fcd06701ae450615881024273629b..87ae254349d5aa37176e2484ffede2f7353122c5 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/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
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 910bb4dfce767536d0ef9979ceed4c5dfab04443..6f8a65f402a6e18c9a8162721f582c3b876e28f5 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/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
diff --git a/src/plugins/value/partitioning/split_return.ml b/src/plugins/value/partitioning/split_return.ml
index fe4ee995d773c8e3bf51c28d2d70101680c6c161..0ecb7b4edfc6a20a1422616d84a3f74aad55bc6e 100644
--- a/src/plugins/value/partitioning/split_return.ml
+++ b/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