[convert] do not translate templated methods that are in fact never instantiated

Actually, they appear only in the AST generated by clang-11.

convert.ml

@@ -40,6 +40,8 @@ let make_lambda_cons_name s1 = s1 ^ "_cons"
 
 let fc_implicit_attr = "__fc_implicit"
 
+let fc_pure_template_decl_attr = "__fc_pure_template_decl"
+
 let capture_name_type env =
   function
   | Cap_id (s, typ, is_ref) ->
@@ -3494,6 +3496,9 @@ let constify_receiver kind args =
     this :: args
   | _ -> args
 
+let is_pure_templated_decl kind body has_further_definition =
+  kind <> TStandard && body = None && not has_further_definition
+
 let rec collect_class_components env body =
   List.fold_left
     convert_class_component (env,[],[],[],[]) (reorder_implicit body)
@@ -3541,6 +3546,8 @@ and convert_class_component (env, implicits, types, fields, others) meth =
       let name =
         if implicit then
           (n,dt,(fc_implicit_attr,[])::a,loc)
+        else if is_pure_templated_decl tkind body has_further_definition then
+          (n,dt, (fc_pure_template_decl_attr,[])::a,loc)
         else name
       in
       let has_virtual_base = Class.has_virtual_base_class class_name in
@@ -4149,7 +4156,7 @@ let convert_ast file =
   Frama_Clang_option.debug ~dkey "Before reordering:@\n%a" Cprint.printFile res;
   Reorder_defs.reorder res
 
-let remove_implicit file =
+let remove_unneeded file =
   let open Cil_types in
   let destructors = ref Datatype.String.Set.empty in
   let rec add_name = function
@@ -4169,8 +4176,9 @@ let remove_implicit file =
   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
+      not (Cil.hasAttribute fc_pure_template_decl_attr v.vattr) &&
+      (not (Cil.hasAttribute fc_implicit_attr v.vattr)
+       || Datatype.String.Set.mem v.vname !destructors)
     | _ -> true
   in
   Rmtmps.removeUnused ~isRoot file

convert.mli

@@ -26,10 +26,19 @@ open Intermediate_format
     by Frama-Clang. *)
 val fc_implicit_attr: string
 
+(** attribute decorating templated member functions that are never defined
+    (i.e. fully instantiated). Their presence in the AST tends to be
+    dependent on the clang version used for type-checking.
+*)
+val fc_pure_template_decl_attr: string
+
 (** creates the name of the field corresponding to a direct base class. *)
 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
+(** remove unneeded definitions and declarations. Notably:
+    - unused implicit definitions
+    - templated member functions that are not defined and never used.
+*)
+val remove_unneeded: Cil_types.file -> unit

frama_Clang_register.ml

@@ -133,6 +133,7 @@ let init_cxx_normalization () =
   if not !is_initialized then begin
       is_initialized:=true;
       Cil_printer.register_shallow_attribute Convert.fc_implicit_attr;
+      Cil_printer.register_shallow_attribute Convert.fc_pure_template_decl_attr;
       Printer.update_printer (module Cxx_printer);
       (* enable exception removal unless it has explicitely been set to false
          on the command line.
@@ -175,7 +176,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;
+  Convert.remove_unneeded cil;
   (cil, cabs)
 
 let cxx_suffixes = [ ".cpp"; ".C"; ".cxx"; ".c++"; ".cc"; ".ii" ]

tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle

@@ -1734,27 +1734,6 @@ void shared_ptr<Aircraft>::Ctor(struct shared_ptr<Aircraft> const *this)
 void shared_ptr<Aircraft>::Ctor(struct shared_ptr<Aircraft> const *this,
                                 struct Aircraft *p);
 
-/*@ requires \separated(this, r);
-    requires \valid_read(this);
-    requires \valid_read(r);
- */
-void shared_ptr<Aircraft>::Ctor(struct shared_ptr<Aircraft> const *this,
-                                struct shared_ptr<Aircraft> const *r);
-
-/*@ requires \separated(this, r);
-    requires \valid_read(this);
-    requires \valid(r);
- */
-void shared_ptr<Aircraft>::Ctor(struct shared_ptr<Aircraft> const *this,
-                                struct shared_ptr<Aircraft> *r)
-{
-  this->__ptr = r->__ptr;
-  this->_ref = r->_ref;
-  r->__ptr = (struct Aircraft *)0;
-  r->_ref = (struct __shared_ref_base *)0;
-  return;
-}
-
 void shared_ptr<Aircraft>::Ctor(struct shared_ptr<Aircraft> const *this,
                                 struct weak_ptr<Aircraft> const *r);
 
@@ -2073,18 +2052,6 @@ void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this)
   return;
 }
 
-/*@ requires \valid_read(this);
-    requires \valid_read(r); */
-void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this,
-                              struct shared_ptr<Aircraft> const *r);
-
-/*@ requires \separated(this, r);
-    requires \valid_read(this);
-    requires \valid_read(r);
- */
-void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this,
-                              struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid_read(this); */
 void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 {
@@ -2105,12 +2072,6 @@ void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 struct weak_ptr<Aircraft> *operator=(struct weak_ptr<Aircraft> *this,
                                      struct weak_ptr<Aircraft> const *r);
 
-/*@ requires \valid(this);
-    requires \valid_read(r);
-    ensures \valid(\result); */
-struct weak_ptr<Aircraft> *operator=<Aircraft,void>(struct weak_ptr<Aircraft> *this,
-                                                    struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid(this);
     requires \valid_read(r);
     ensures __fc_exn.exn_uncaught ≡ 0 ⇒ \valid(\result);

tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle

@@ -2014,13 +2014,6 @@ void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this)
   return;
 }
 
-/*@ requires \separated(this, r);
-    requires \valid_read(this);
-    requires \valid_read(r);
- */
-void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this,
-                              struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid_read(this); */
 void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 {
@@ -2039,12 +2032,6 @@ void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 struct weak_ptr<Aircraft> *operator=(struct weak_ptr<Aircraft> *this,
                                      struct weak_ptr<Aircraft> const *r);
 
-/*@ requires \valid(this);
-    requires \valid_read(r);
-    ensures \valid(\result); */
-struct weak_ptr<Aircraft> *operator=<Aircraft,void>(struct weak_ptr<Aircraft> *this,
-                                                    struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid(this);
     requires \valid(r); */
 void swap(struct weak_ptr<Aircraft> *this, struct weak_ptr<Aircraft> *r);

tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle

@@ -2020,13 +2020,6 @@ void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this)
   return;
 }
 
-/*@ requires \separated(this, r);
-    requires \valid_read(this);
-    requires \valid_read(r);
- */
-void weak_ptr<Aircraft>::Ctor(struct weak_ptr<Aircraft> const *this,
-                              struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid_read(this); */
 void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 {
@@ -2045,12 +2038,6 @@ void weak_ptr<Aircraft>::Dtor(struct weak_ptr<Aircraft> const *this)
 struct weak_ptr<Aircraft> *operator=(struct weak_ptr<Aircraft> *this,
                                      struct weak_ptr<Aircraft> const *r);
 
-/*@ requires \valid(this);
-    requires \valid_read(r);
-    ensures \valid(\result); */
-struct weak_ptr<Aircraft> *operator=<Aircraft,void>(struct weak_ptr<Aircraft> *this,
-                                                    struct weak_ptr<Aircraft> const *r);
-
 /*@ requires \valid(this);
     requires \valid(r); */
 void swap(struct weak_ptr<Aircraft> *this, struct weak_ptr<Aircraft> *r);

tests/stl/oracle/stl_utility.res.oracle

@@ -950,29 +950,6 @@ void pair<int&,bool>::Ctor(struct pair<int&,bool> const *this, int *x,
   return;
 }
 
-/*@ requires \valid_read(this);
-    requires \valid_read(p); */
-void pair<int&,bool>::Ctor(struct pair<int&,bool> const *this,
-                           struct pair<int,bool> const *p);
-
-/*@ requires \valid(this);
-    requires \valid_read(p);
-    ensures \valid(\result); */
-struct pair<int&,bool> *operator=<int&,bool,void>(struct pair<int&,bool> *this,
-                                                  struct pair<int&,bool> const *p);
-
-/*@ requires \valid(this);
-    requires \valid_read(p);
-    ensures \valid(\result); */
-struct pair<int&,bool> *operator=<int,bool,void>(struct pair<int&,bool> *this,
-                                                 struct pair<int,bool> const *p);
-
-/*@ requires \valid(this);
-    requires \valid(p);
-    ensures \valid(\result); */
-struct pair<int&,bool> *operator=<int&,bool,void>(struct pair<int&,bool> *this,
-                                                  struct pair<int&,bool> *p);
-
 struct pair<int&,bool> *operator=<int,bool,void>(struct pair<int&,bool> *this,
                                                  struct pair<int,bool> *p);