diff --git a/convert.ml b/convert.ml
index 3aae9f5de0f77a849252ace41523709ba1fdf992..2d3529962075fd941631d0dffdd83541eb15f0be 100644
--- a/convert.ml
+++ b/convert.ml
@@ -2702,14 +2702,6 @@ let is_implicit_func = function
   | CMethod(_,_,_,_,_,_,_,b,_,_,_,_) -> b
   | _ -> false
 
-let extract_decl = function
-  | CMethod(loc,name, kind,rt,args,variadic,_,_,tkind,has_further_definition,
-      _,_) ->
-    (* If any, the spec will still be ported by the original declaration. *)
-    CMethod(loc,name,kind,rt,args,variadic,None,false,tkind,
-            has_further_definition,None,None)
-  | c -> c
-
 let implicit_kind = function
   | CMethod(_,_,kind,_,args,_,_,_,_,_,_,_) ->
     (match kind, args with
@@ -2773,9 +2765,9 @@ let cmp_implicit i1 i2 =
   compare n1 n2
 
 let reorder_implicit l =
-  let implicit = Extlib.filter_map is_implicit_func extract_decl l in
+  let implicit,others = List.partition is_implicit_func l in
   let implicit = List.stable_sort cmp_implicit implicit in
-  implicit @ l
+  implicit @ others
 
 let iter_on_array ?(incr=true) env idx length mk_body =
   let loc = Convert_env.get_loc env in
diff --git a/tests/basic/oracle/c_link.res.oracle b/tests/basic/oracle/c_link.res.oracle
index cdd0578f1d993f6d1fd4a69fc1e392170a441d38..7d0032c420ff804ef469cfb77ae8983ca84f8c23 100644
--- a/tests/basic/oracle/c_link.res.oracle
+++ b/tests/basic/oracle/c_link.res.oracle
@@ -49,12 +49,6 @@ void Foo::Ctor(struct Foo const *this)
   return;
 }
 
-/*@ requires \valid_read(this); */
-void Foo::Dtor(struct Foo const *this)
-{
-  return;
-}
-
 /*@ requires \valid(this);
     requires \valid(__frama_c_arg_0);
     ensures \valid(\result);
@@ -65,6 +59,12 @@ struct Foo *operator=(struct Foo *this, struct Foo *__frama_c_arg_0)
   return this;
 }
 
+/*@ requires \valid_read(this); */
+void Foo::Dtor(struct Foo const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "Foo",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/basic/oracle/pointer_to_member.res.oracle b/tests/basic/oracle/pointer_to_member.res.oracle
index c05062e31860af5d35b9f78f76b25f4bfa7524ce..9649b6157d88b29ce998e0b8f05820e9b7ebd422 100644
--- a/tests/basic/oracle/pointer_to_member.res.oracle
+++ b/tests/basic/oracle/pointer_to_member.res.oracle
@@ -51,14 +51,14 @@ void m(struct Foo *this, int i)
 }
 
 /*@ requires \valid_read(this); */
-void Foo::Dtor(struct Foo const *this)
+void Foo::Ctor(struct Foo const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void Foo::Ctor(struct Foo const *this)
+void Foo::Dtor(struct Foo const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
@@ -309,18 +309,18 @@ void m(struct Bar *this, int i)
 }
 
 /*@ requires \valid_read(this); */
-void Bar::Dtor(struct Bar const *this)
+void Bar::Ctor(struct Bar const *this)
 {
+  Foo::Ctor(& this->_frama_c__Z3Foo);
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
-  Foo::Dtor(& this->_frama_c__Z3Foo);
   return;
 }
 
 /*@ requires \valid_read(this); */
-void Bar::Ctor(struct Bar const *this)
+void Bar::Dtor(struct Bar const *this)
 {
-  Foo::Ctor(& this->_frama_c__Z3Foo);
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  Foo::Dtor(& this->_frama_c__Z3Foo);
   return;
 }
 
diff --git a/tests/basic/oracle/pointer_to_virtual_method.res.oracle b/tests/basic/oracle/pointer_to_virtual_method.res.oracle
index 56e749cb781bf252cb4b86f351f9df949b20f176..93a3d5a15ef5d1728e91a3142ab69fee97323bed 100644
--- a/tests/basic/oracle/pointer_to_virtual_method.res.oracle
+++ b/tests/basic/oracle/pointer_to_virtual_method.res.oracle
@@ -49,14 +49,14 @@ void m(struct Foo *this, int i)
 }
 
 /*@ requires \valid_read(this); */
-void Foo::Dtor(struct Foo const *this)
+void Foo::Ctor(struct Foo const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void Foo::Ctor(struct Foo const *this)
+void Foo::Dtor(struct Foo const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
@@ -307,18 +307,18 @@ void m(struct Bar *this, int i)
 }
 
 /*@ requires \valid_read(this); */
-void Bar::Dtor(struct Bar const *this)
+void Bar::Ctor(struct Bar const *this)
 {
+  Foo::Ctor(& this->_frama_c__Z3Foo);
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
-  Foo::Dtor(& this->_frama_c__Z3Foo);
   return;
 }
 
 /*@ requires \valid_read(this); */
-void Bar::Ctor(struct Bar const *this)
+void Bar::Dtor(struct Bar const *this)
 {
-  Foo::Ctor(& this->_frama_c__Z3Foo);
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
+  Foo::Dtor(& this->_frama_c__Z3Foo);
   return;
 }
 
diff --git a/tests/class/oracle/constr.res.oracle b/tests/class/oracle/constr.res.oracle
index 8e5eda82c40e982ddd0964a70317dc243a802c7d..9bc61b0334192fe4b29e80a61fb00cd2e90803d9 100644
--- a/tests/class/oracle/constr.res.oracle
+++ b/tests/class/oracle/constr.res.oracle
@@ -41,12 +41,6 @@ void Foo::Ctor(struct Foo const *this, int a)
   return;
 }
 
-/*@ requires \valid_read(this); */
-void Foo::Dtor(struct Foo const *this)
-{
-  return;
-}
-
 /*@ requires \valid(this);
     requires \valid(__frama_c_arg_0);
     ensures \valid(\result);
@@ -57,6 +51,12 @@ struct Foo *operator=(struct Foo *this, struct Foo *__frama_c_arg_0)
   return this;
 }
 
+/*@ requires \valid_read(this); */
+void Foo::Dtor(struct Foo const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "Foo",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/class/oracle/inheritance_out_def.res.oracle b/tests/class/oracle/inheritance_out_def.res.oracle
index c8a22ff4c9abba325131da43222c3286513c53e7..3fed02e862fdd349ad0d9c23d36595104edaf5e2 100644
--- a/tests/class/oracle/inheritance_out_def.res.oracle
+++ b/tests/class/oracle/inheritance_out_def.res.oracle
@@ -51,14 +51,14 @@ int get_sum(struct A *this)
 }
 
 /*@ requires \valid_read(this); */
-void A::Dtor(struct A const *this)
+void A::Ctor(struct A const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void A::Ctor(struct A const *this)
+void A::Dtor(struct A const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 3aa54b20c452e6755f0fe246cec438b891e24943..cb1bcd15932e014f92ca3a84c003627cd395ff70 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -2238,12 +2238,6 @@ void __bool_binop<int,std::__equal_to>::Ctor(struct __bool_binop<int,std::__equa
   return;
 }
 
-/*@ requires \valid_read(this); */
-void __bool_binop<int,std::__equal_to>::Dtor(struct __bool_binop<int,std::__equal_to> const *this)
-{
-  return;
-}
-
 /*@ requires \separated(this, __frama_c_arg_0);
     requires \valid_read(this);
     requires \valid_read(__frama_c_arg_0);
@@ -2254,6 +2248,12 @@ void __bool_binop<int,std::__equal_to>::Ctor(struct __bool_binop<int,std::__equa
   return;
 }
 
+/*@ requires \valid_read(this); */
+void __bool_binop<int,std::__equal_to>::Dtor(struct __bool_binop<int,std::__equal_to> const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "__bool_binop",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 21d7a5ac23f49d50873cec5944fa19f3c036f2a0..fd7d8e7118aa015352efd8c7bd6fd7eedd426fe6 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -2003,12 +2003,6 @@ void __binop<int,std::__minus>::Ctor(struct __binop<int,std::__minus> const *thi
   return;
 }
 
-/*@ requires \valid_read(this); */
-void __binop<int,std::__minus>::Dtor(struct __binop<int,std::__minus> const *this)
-{
-  return;
-}
-
 /*@ requires \separated(this, __frama_c_arg_0);
     requires \valid_read(this);
     requires \valid(__frama_c_arg_0);
@@ -2019,6 +2013,12 @@ void __binop<int,std::__minus>::Ctor(struct __binop<int,std::__minus> const *thi
   return;
 }
 
+/*@ requires \valid_read(this); */
+void __binop<int,std::__minus>::Dtor(struct __binop<int,std::__minus> const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "__binop",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
@@ -2050,12 +2050,6 @@ void __binop<int,std::__plus>::Ctor(struct __binop<int,std::__plus> const *this)
   return;
 }
 
-/*@ requires \valid_read(this); */
-void __binop<int,std::__plus>::Dtor(struct __binop<int,std::__plus> const *this)
-{
-  return;
-}
-
 /*@ requires \separated(this, __frama_c_arg_0);
     requires \valid_read(this);
     requires \valid(__frama_c_arg_0);
@@ -2066,6 +2060,12 @@ void __binop<int,std::__plus>::Ctor(struct __binop<int,std::__plus> const *this,
   return;
 }
 
+/*@ requires \valid_read(this); */
+void __binop<int,std::__plus>::Dtor(struct __binop<int,std::__plus> const *this)
+{
+  return;
+}
+
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
   {.name = "__binop",
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
diff --git a/tests/stl/oracle/stl_iterator.res.oracle b/tests/stl/oracle/stl_iterator.res.oracle
index 68dbb1b1d9c26f30d962cc1e88240bf8e8035ff9..78567b1ae7b4333b03e22826238239c9ee7b6402 100644
--- a/tests/stl/oracle/stl_iterator.res.oracle
+++ b/tests/stl/oracle/stl_iterator.res.oracle
@@ -336,7 +336,7 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
 struct _frama_c_vmt_content _frama_c_vmt[1];
 /*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
 (struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
 {
   return;
@@ -354,7 +354,7 @@ void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
 }
 
 /*@ requires \valid_read(this); */
-void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Ctor
+void iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor
 (struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *this)
 {
   return;
@@ -430,13 +430,6 @@ _Bool operator<<int*,void>(struct reverse_iterator<int*> *this,
   return __retres;
 }
 
-/*@ requires \valid_read(this); */
-void reverse_iterator<int*>::Dtor(struct reverse_iterator<int*> const *this)
-{
-  iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(& this->_frama_c__ZN3stdE8iteratorIN3stdE26random_access_iterator_tagiiPKiRKiE);
-  return;
-}
-
 /*@ requires \separated(this, __frama_c_arg_0);
     requires \valid_read(this);
     requires \valid_read(__frama_c_arg_0);
@@ -451,6 +444,13 @@ void reverse_iterator<int*>::Ctor(struct reverse_iterator<int*> const *this,
   return;
 }
 
+/*@ requires \valid_read(this); */
+void reverse_iterator<int*>::Dtor(struct reverse_iterator<int*> const *this)
+{
+  iterator<std::random_access_iterator_tag,int,int,int*,int&>::Dtor(& this->_frama_c__ZN3stdE8iteratorIN3stdE26random_access_iterator_tagiiPKiRKiE);
+  return;
+}
+
 /*@ requires \valid(this); */
 struct reverse_iterator<int*> operator++(struct reverse_iterator<int*> *this,
                                          int __frama_c_arg_0)
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index c042591d8edbfc2968e99f54b2b05e6bb34e6f6d..d155ac18a8a844ebe73a7649fa9ceddf59a0274a 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -1853,14 +1853,14 @@ void *get_deleter(struct __shared_ref_base *this)
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
+void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
+void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index c0312ae75ac14203b6c0b263a7bd308490963565..62dc277cc040a88d2573c803f90b11ef0c438ef4 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -1811,14 +1811,14 @@ void *get_deleter(struct __shared_ref_base *this)
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
+void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
+void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index e2653bc827f44c07694449142110470c57e38928..9d26c14a70048ce5ca6e1723e0baf41afeffc227 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -1817,14 +1817,14 @@ void *get_deleter(struct __shared_ref_base *this)
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
+void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;
 }
 
 /*@ requires \valid_read(this); */
-void __shared_ref_base::Ctor(struct __shared_ref_base const *this)
+void __shared_ref_base::Dtor(struct __shared_ref_base const *this)
 {
   *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
   return;