diff --git a/convert.ml b/convert.ml
index 2d3529962075fd941631d0dffdd83541eb15f0be..c251a175190468813a87a5d093c75ab6897d1e73 100644
--- a/convert.ml
+++ b/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
diff --git a/convert.mli b/convert.mli
index 987382943598f8fe4060fe56f7a7d1e31819200d..931700b0763448b1854fa7cab5c66cede04e6773 100644
--- a/convert.mli
+++ b/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
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index de3b86f72a293be405a8670f907c2836cc2f738d..ebb6281abfaad93c346314cc3d72cd4168cc143a 100644
--- a/frama_Clang_register.ml
+++ b/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" ]
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index d155ac18a8a844ebe73a7649fa9ceddf59a0274a..4adbb86fb77dcb1e41d4ff3db69e1c6b31813007 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/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);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 62dc277cc040a88d2573c803f90b11ef0c438ef4..4402c8aeace38b401b7dbb1c1b7f795ae5ec241a 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/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);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 9d26c14a70048ce5ca6e1723e0baf41afeffc227..8784981af35674592d6b5c0686f87545ddda83b4 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/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);
diff --git a/tests/stl/oracle/stl_utility.res.oracle b/tests/stl/oracle/stl_utility.res.oracle
index 69dc88fa52bb4dab6386e234cc99df078bb6d365..2b79ae2cd02f09ea67f0031741708f01dba38dad 100644
--- a/tests/stl/oracle/stl_utility.res.oracle
+++ b/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);