From c15d72bc18ee7fb78a0651b81cf60ed303faa643 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Feb 2021 13:10:44 +0100
Subject: [PATCH] [conversion] do not keep implicit members if they're not
 used.

---
 convert.ml              | 31 ++++++++++++++++++++++++++++++-
 convert.mli             |  3 +++
 frama_Clang_register.ml |  1 +
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/convert.ml b/convert.ml
index 585825b..ffd3fbf 100644
--- a/convert.ml
+++ b/convert.ml
@@ -38,6 +38,8 @@ let new_lambda_def_name = fresh_names lambda_def_name
 
 let make_lambda_cons_name s1 = s1 ^ "_cons"
 
+let fc_implicit_attr = "__fc_implicit"
+
 let capture_name_type env =
   function
   | Cap_id (s, typ, is_ref) ->
@@ -2925,11 +2927,12 @@ and create_generic_op op env most_derived class_name =
       Convert_env.fatal
         env "Unexpected number of arguments for an implicit member function"
   in
-  let env, (rt, defname) =
+  let env, (rt, (n,dt,attrs,loc)) =
     make_prototype
       (Convert_env.get_loc env) env cname kind signature.result
       args signature.variadic false
   in
+  let defname = (n,dt,(fc_implicit_attr,[])::attrs,loc) in
   let ret_stmt = op.return () in
   let body, defs, env =
     if is_union then begin
@@ -4085,3 +4088,29 @@ let convert_ast file =
   let dkey = Frama_Clang_option.dkey_reorder in
   Frama_Clang_option.debug ~dkey "Before reordering:@\n%a" Cprint.printFile res;
   Reorder_defs.reorder res
+
+let remove_implicit file =
+  let open Cil_types in
+  let destructors = ref Datatype.String.Set.empty in
+  let rec add_name = function
+    | AAddrOf a -> add_name a
+    | AStr f -> destructors:= Datatype.String.Set.add f !destructors
+    | ACons(f,_) -> destructors:=Datatype.String.Set.add f !destructors
+    | _ -> ()
+  in
+  let collect_destructors = object
+    inherit Cil.nopCilVisitor
+    method! vattr = function
+      | Attr(s,[d]) when s = Cabs2cil.frama_c_destructor ->
+        add_name d; Cil.SkipChildren
+      | _ -> Cil.SkipChildren
+  end
+  in
+  Cil.visitCilFileSameGlobals collect_destructors file;
+  let isRoot = function
+    | GFunDecl(_,v,_) | GFun ({svar = v},_) ->
+      not (Cil.hasAttribute fc_implicit_attr v.vattr)
+      || Datatype.String.Set.mem v.vname !destructors
+    | _ -> true
+  in
+  Rmtmps.removeUnused ~isRoot file
diff --git a/convert.mli b/convert.mli
index eefca7f..c10b129 100644
--- a/convert.mli
+++ b/convert.mli
@@ -26,3 +26,6 @@ open Intermediate_format
 val create_base_field_name: Convert_env.env -> qualified_name -> tkind -> string
  
 val convert_ast: Intermediate_format.file -> Cabs.file
+
+(** remove unused implicit definitions. *)
+val remove_implicit: Cil_types.file -> unit
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index d51c0d5..8362a93 100644
--- a/frama_Clang_register.ml
+++ b/frama_Clang_register.ml
@@ -174,6 +174,7 @@ let parse_cxx file =
   Frama_Clang_option.feedback ~dkey "Generated Cabs code:@\n%a"
     Cprint.printFile cabs;
   let cil = Cabs2cil.convFile cabs in
+  Convert.remove_implicit cil;
   (cil, cabs)
 
 let cxx_suffixes = [ ".cpp"; ".C"; ".cxx"; ".c++"; ".cc"; ".ii" ]
-- 
GitLab