From 1b96e30d284356a7cc152063a56beec3dff65907 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Sun, 16 Jan 2022 12:44:32 +0100 Subject: [PATCH] [kernel] Optimizes the [expand_destructors] code transformation. Only visits function definitions: avoids visiting the specifications of the Frama-C libc. --- src/kernel_services/analysis/destructors.ml | 29 +++++++++------------ 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml index 379bca768b4..45685314bef 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" -- GitLab