diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index c1d3ff0b7ffbed81bc08abe03a50a46cf823f70d..6862e67bc672164958fbd56af4ff91629c267db0 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 c14ea9fc19fa6951f6128f388462e0e42004f793..0281d236c8435f0b70b14dde140f526197985c58 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/cfg.ml b/src/kernel_internals/typing/cfg.ml
index d9cb57f9193b322f97e4f69dbc54ca15714123a6..d0e7b4da779fb0548edf2fe50b0306a557970e7f 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -307,6 +307,13 @@ let forallStmts todo (fd : fundec) =
let vis = object
inherit nopCilVisitor
method! vstmt stmt = ignore (todo stmt); DoChildren
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
+ method! vattr _ = SkipChildren
end
in
ignore (visitCilFunction vis fd)
@@ -744,6 +751,7 @@ class registerLabelsVisitor : cilVisitor = object
method! vexpr _ = SkipChildren
method! vtype _ = SkipChildren
method! vinst _ = SkipChildren
+ method! vspec _ = SkipChildren
method! vcode_annot _ = SkipChildren (* via Loop stmt *)
method! vlval _ = SkipChildren (* via UnspecifiedSequence stmt *)
method! vattr _ = SkipChildren (* via block stmt *)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 00e4e2de03398fa88074ae5b9176c9e0c37c7993..8330edfe5e0c254f444498a1b506f6a860e161df 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -121,7 +121,7 @@ class visitor = object(self)
Error.cannot_check_ghost_call ~source ~current:true ~once:true kf
method! vglob_aux = function
- | GFunDecl(_, vi, _) ->
+ | GFunDecl(_, vi, _) when vi.vghost ->
self#prefer_loc (Log.get_current_source ()) ;
let post g = self#reset_loc() ; g in
@@ -136,7 +136,11 @@ class visitor = object(self)
if is_empty_funspec spec then self#bad_ghost_function kf
end ;
Cil.DoChildrenPost post
- | _ -> Cil.DoChildren
+ (* Optimization: only visits ghost globals or globals that may contain
+ ghost code. *)
+ | GVarDecl (vi, _) when vi.vghost -> Cil.DoChildren
+ | GVar _ | GFun _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
method! vvdec v =
let current, source =
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 0bef4ca0188388bd11ccd2315ad6a9c9d4bfb3f3..83a59cde83fddd66975eea7b3d8834ccea9ae4b9 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -581,7 +581,7 @@ let global_type_and_name = function
| GText _ -> "<text>"
| GAnnot _ -> "<annot>"
-class markReferencedVisitor = object
+class markReferencedVisitor = object (self)
inherit nopCilVisitor
val dkey = Kernel.dkey_referenced
@@ -589,6 +589,13 @@ class markReferencedVisitor = object
val inside_exp : exp Stack.t = Stack.create ()
val inside_typ : typ Stack.t = Stack.create ()
+ method private reference varinfo loc =
+ if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then begin
+ Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
+ Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
+ varinfo.vreferenced <- true;
+ end
+
method! vglob = function
| GType (typeinfo, loc) ->
Kernel.debug ~source:(fst loc) ~dkey "referenced: type %s" typeinfo.tname;
@@ -604,19 +611,14 @@ class markReferencedVisitor = object
Kernel.debug ~source:(fst loc) ~dkey "referenced: enum %s" enuminfo.ename;
enuminfo.ereferenced <- true;
DoChildren
- | GVar (varinfo, _, loc)
- | GVarDecl (varinfo, loc)
- | GFunDecl (_,varinfo, loc)
- | GFun ({svar = varinfo}, loc) ->
- if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then begin
- Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
- Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
- varinfo.vreferenced <- true;
- end;
+ | GVar (varinfo, _, loc) | GFun ({svar = varinfo}, loc) ->
+ self#reference varinfo loc;
DoChildren
- | GAnnot _ -> DoChildren
- | _ ->
+ | GVarDecl (varinfo, loc)
+ | GFunDecl (_,varinfo, loc) ->
+ self#reference varinfo loc;
SkipChildren
+ | _ -> SkipChildren
method! vtype = function
| TNamed (ti, _) ->
@@ -661,6 +663,8 @@ class markReferencedVisitor = object
end;
SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let markReferenced ast =
diff --git a/src/kernel_internals/typing/substitute_const_globals.ml b/src/kernel_internals/typing/substitute_const_globals.ml
index e801e61e7738f00b39c3aecbe8851e5157463d19..d9ba1dcc88cfbdb3006ef40101abd4dfd0837660 100644
--- a/src/kernel_internals/typing/substitute_const_globals.ml
+++ b/src/kernel_internals/typing/substitute_const_globals.ml
@@ -59,8 +59,8 @@ class constGlobSubstVisitorClass : cilVisitor = object
if is_arithmetic_type typ && isConstType typ
then ChangeDoChildrenPost ([g], List.map register)
else DoChildren
- | _ ->
- DoChildren
+ | GFun _ -> DoChildren
+ | _ -> SkipChildren
(* Visit expressions and replace lvals, with a registered varinfo in
[vi_to_init_opt], with respective initializing constant expressions. *)
@@ -104,6 +104,10 @@ class constGlobSubstVisitorClass : cilVisitor = object
end
| _ ->
DoChildren
+
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let constGlobSubstVisitor = new constGlobSubstVisitorClass
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 96fec8b12070cabdab194ef7a59b63376cda5339..4ebac5d58b904bbf9f88bb7ba3e01eeec30554fb 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/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 1cd59c9c039b5d25ae133d0ac3065c0bb111dbaf..b03bdaa56e7cd620e467f3cdf8cc713743e6e9e7 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -279,22 +279,19 @@ class vis flag = object(self)
end
-let treat_one_function flag kf =
- if not (Cil_builtins.is_special_builtin (Kernel_function.get_name kf))
- then begin
- let my_flag = ref false in
- let vis = new vis my_flag in
- ignore (Visitor.visitFramacKf vis kf);
- if !my_flag then begin
- flag := true;
- File.must_recompute_cfg (Kernel_function.get_definition kf)
- end
- end
-
-let add_destructor _ast =
- let has_grown = ref false in
- Globals.Functions.iter (treat_one_function has_grown);
- if !has_grown then Ast.mark_as_grown ()
+let add_destructor file =
+ let is_builtin fundec = Cil_builtins.is_special_builtin fundec.svar.vname in
+ let process_one_global has_grown = function
+ | GFun (fundec, _) when not (is_builtin fundec) ->
+ let flag = ref false in
+ let visitor = new vis flag in
+ ignore (Visitor.visitFramacFunction visitor fundec);
+ if !flag then File.must_recompute_cfg fundec;
+ has_grown || !flag
+ | _ -> has_grown
+ in
+ let has_grown = Cil.foldGlobals file process_one_global false in
+ if has_grown then Ast.mark_as_grown ()
let transform_category =
File.register_code_transformation_category "expand_destructors"
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 9e54918cf30b0c895aa68c4ec5c4da6040cecac3..5adfcc1b04d46ee3b924cd6b4ef3701d6d3de1f7 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/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml
index 8a86691d3228fef1c3577a7475e12f9d418ce065..ef71fa89e876a5330a637a724f741c600122df38 100644
--- a/src/kernel_services/analysis/undefined_sequence.ml
+++ b/src/kernel_services/analysis/undefined_sequence.ml
@@ -143,6 +143,13 @@ let check_sequences file =
(my_stmt_print#without_annot my_stmt_print#stmt) s
| _ -> ());
Cil.DoChildren
+
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
in
- Cil.visitCilFileSameGlobals check_unspec file
+ Cil.visitCilFileFunctions check_unspec file
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index 3345b02185742a73fc313a99089f6921d305a740..14f9ade3b3b2add5e0bb8ca88a8949a6139ed5da 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -142,19 +142,23 @@ let compute () =
method! vstmt s =
Datatype.Int.Hashtbl.add h s.sid (self#kf, s, opened_blocks);
Cil.DoChildren
- method! vglob g =
- begin match g with
- | GFun (fd, _) ->
- (try
- let kf = Globals.Functions.get fd.svar in
- current_kf <- Some kf;
- with Not_found ->
- Kernel.fatal "No kernel function for function %a"
- Cil_datatype.Varinfo.pretty fd.svar)
- | _ ->
- ()
- end;
- Cil.DoChildren
+ method! vglob = function
+ | GFun (fd, _) ->
+ (try
+ let kf = Globals.Functions.get fd.svar in
+ current_kf <- Some kf;
+ Cil.DoChildren
+ with Not_found ->
+ Kernel.fatal "No kernel function for function %a"
+ Cil_datatype.Varinfo.pretty fd.svar)
+ | GVar _ -> Cil.SkipChildren
+ | _ -> Cil.SkipChildren
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
in
Cil.visitCilFile (visitor :> Cil.cilVisitor) p;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f2aef10880a544801388ad2e04cbf0aab0dab5c5..daae7bfac546a9972ea6f529488d8f9a7511a9cb 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5262,6 +5262,14 @@ class constFoldVisitorClass (machdep: bool) : cilVisitor = object
(* Do it bottom up *)
ChangeDoChildrenPost (e, constFold machdep)
+ (* Optimization: only visits function and variable definitions. *)
+ method! vglob = function
+ | GFun _ | GVar _ -> DoChildren
+ | _ -> SkipChildren
+
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let constFoldVisitor (machdep: bool) = new constFoldVisitorClass machdep
@@ -5356,6 +5364,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
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index ddd9546b1acc237c1302cdfef1a546d52b2899c7..c3cace34893b20ffbcdc21cb9041c3499c5abcf1 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -991,7 +991,7 @@ let cleanup file =
DoChildren
| GFunDecl(s,_,_) ->
Logic_utils.clear_funspec s;
- DoChildren
+ SkipChildren
| GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _
| GEnumTagDecl _ | GVar _ | GVarDecl _ | GAsm _ | GPragma _ | GText _
| GAnnot _ ->
@@ -1003,6 +1003,13 @@ let cleanup file =
Cfg.clearFileCFG ~clear_id:false f;
Cfg.computeFileCFG f; f end
else f)
+
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
in visitFramacFileSameGlobals visitor file
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index f17c14086a3683ef1fb6a8527379330e36aebb25..954673433e980f2412f420c70e5c15b5d6689138 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2349,6 +2349,15 @@ class complete_types =
not (isLogicType Cil.isCompleteType t.term_type) ->
ChangeDoChildrenPost({ t with term_type = v.lv_type }, fun x -> x)
| _ -> DoChildrenPost self#insert_cast_term
+
+ method! vinst = function
+ | Code_annot _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
+ method! vexpr _ = Cil.SkipChildren
+ method! vlval _ = Cil.SkipChildren
+ method! vtype _ = Cil.SkipChildren
+ method! vinit _ _ _ = Cil.SkipChildren
end
let complete_types f = Cil.visitCilFile (new complete_types) f
diff --git a/src/kernel_services/ast_transformations/contract_special_float.ml b/src/kernel_services/ast_transformations/contract_special_float.ml
index f7a1cf660b9e9b402a449f8a921e4d1f4f09d31a..6388ac7d93eeeb64dfc7c17808c750b6a9040ac3 100644
--- a/src/kernel_services/ast_transformations/contract_special_float.ml
+++ b/src/kernel_services/ast_transformations/contract_special_float.ml
@@ -121,14 +121,14 @@ let update_spec spec =
spec.spec_complete_behaviors <- map_filter spec.spec_complete_behaviors;
spec.spec_disjoint_behaviors <- map_filter spec.spec_disjoint_behaviors
-let visitor = object
- inherit Cil.nopCilVisitor
- method! vspec spec = update_spec spec; Cil.SkipChildren
-end
+let visit_global = function
+ | GFun (fundec, _) -> update_spec fundec.sspec
+ | GFunDecl (spec, _, _) -> update_spec spec
+ | _ -> ()
let run ast =
if Kernel.SpecialFloat.get () <> "none" then
- Cil.visitCilFileSameGlobals visitor ast
+ Cil.iterGlobals ast visit_global
let transform =
File.register_code_transformation_category "contract_special_float"
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 74e216b8a3fb35e1f0e5f80104a6060c3a63f35a..c4d70589e7d2ece6eb332abbf9cb94b54060d082 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 2687e11d6c366c2dbc9a8f134ae310d9d9392bd1..cbfdfbc2c3f0d07e732ec888097fcac4845d81ec 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 7c56409b78dcc66493d95bec0201a5e2719256a3..b74ea02520e42e60058b9e634f6ae417c78c305b 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/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 7cfe249b8fe0f65db3923253da1605917e4885d4..c48bc00ff4efd4552ff5bdff6c72ef144c57154b 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -679,7 +679,6 @@ let add_global glob = globals_queue := glob :: !globals_queue
(* Utilities for global variables *)
let add_gvar ?init vi =
let initinfo = {Cil_types.init} in
- vi.vghost <- true;
vi.vstorage <- NoStorage;
add_global (GVar(vi,initinfo,vi.vdecl));
Globals.Vars.add vi initinfo;
@@ -700,7 +699,7 @@ let mk_gvar ?init ~ty name =
Globals.Vars.remove vi;
vi
with Not_found ->
- Cil.makeGlobalVar name ty
+ Cil.makeGlobalVar ~ghost:true name ty
in
add_gvar ?init vi
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index eefa9a3fc5780584bf2953cf4ada99cbf2963f9f..96f4b22d28ff03e4d2913087d47212a6109d2fa9 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -99,7 +99,7 @@ module State_var =
end)
let get_state_var =
- let add_var state = Cil.makeVarinfo true false state.name Cil.intType in
+ let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil.intType in
State_var.memo add_var
let get_state_logic_var state = Cil.cvar_to_lvar (get_state_var state)
@@ -339,7 +339,9 @@ let pebble_set_at li lab =
let memo_multi_state st =
match st.multi_state with
| None ->
- let aux = Cil.makeGlobalVar (get_fresh "aorai_aux") Cil.intType in
+ let aux =
+ Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil.intType
+ in
let laux = Cil.cvar_to_lvar aux in
let set = Cil_const.make_logic_info (get_fresh (st.name ^ "_pebble")) in
let typ = Logic_const.make_set_type (Ctype Cil.intType) in
@@ -572,7 +574,7 @@ let memo_aux_variable tr counter used_prms vi =
| Some _ -> TArray(vi.vtype,None,[])
in
let my_var =
- Cil.makeGlobalVar (get_fresh ("aorai_" ^ vi.vname)) my_type
+ Cil.makeGlobalVar ~ghost:true (get_fresh ("aorai_" ^ vi.vname)) my_type
in
add_aux_variable my_var;
let my_lvar = Cil.cvar_to_lvar my_var in
@@ -1156,7 +1158,9 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
else Cil.intType
in (* We won't always need a counter *)
lazy (
- let vi = Cil.makeGlobalVar (get_fresh "aorai_counter") ty in
+ let
+ vi = Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_counter") ty
+ in
add_aux_variable vi;
vi
)
@@ -1358,6 +1362,7 @@ let type_trans auto metaenv env tr =
let start = tr.start in
let count = (* TODO: make it an integer. *)
Cil.makeGlobalVar
+ ~ghost:true
(get_fresh ("aorai_cnt_" ^ start.name)) Cil.intType
in
add_aux_variable count;
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index d6e9ea41c6507efce246770655a81c57c7abc0c4..de1e17e53b9052983dc77559907f14a76c48dbb8 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -100,7 +100,10 @@ let add_metavariable map (name,typename) =
in
if Datatype.String.Map.mem name map then
Aorai_option.abort "The metavariable %s is declared twice" name;
- let vi = Cil.makeGlobalVar (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty in
+ let vi =
+ Cil.makeGlobalVar
+ ~ghost:true (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty
+ in
Datatype.String.Map.add name vi map
let check_state st =
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index c00051a00c9b21b7cd93a1888f7c0342ed708c1e..55241baccf115f201dc45a7fc07f990e3c3f2349 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 c2a9b52fff33a23d242258d08f301e674e906b96..e2bbd2b7612c2cce1437d543895c5b7e2490d4cd 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