From 4b08b12e9464f1c0da32519f11a4efb36de68694 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Feb 2021 19:13:41 +0100
Subject: [PATCH] [convert] do not convey multiple decl of implicit members
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

especially if half of them are not seen as implicit afterwards. This can't end
well 😬
---
 convert.ml                                    | 12 ++--------
 tests/basic/oracle/c_link.res.oracle          | 12 +++++-----
 .../basic/oracle/pointer_to_member.res.oracle | 12 +++++-----
 .../pointer_to_virtual_method.res.oracle      | 12 +++++-----
 tests/class/oracle/constr.res.oracle          | 12 +++++-----
 .../oracle/inheritance_out_def.res.oracle     |  4 ++--
 tests/stl/oracle/stl_algorithm.res.oracle     | 12 +++++-----
 tests/stl/oracle/stl_functional.res.oracle    | 24 +++++++++----------
 tests/stl/oracle/stl_iterator.res.oracle      | 18 +++++++-------
 .../stl_shared_ptr_mistake10.res.oracle       |  4 ++--
 .../oracle/stl_shared_ptr_mistake5.res.oracle |  4 ++--
 .../oracle/stl_shared_ptr_mistake6.res.oracle |  4 ++--
 12 files changed, 61 insertions(+), 69 deletions(-)

diff --git a/convert.ml b/convert.ml
index 3aae9f5d..2d352996 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 cdd0578f..7d0032c4 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 c05062e3..9649b615 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 56e749cb..93a3d5a1 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 8e5eda82..9bc61b03 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 c8a22ff4..3fed02e8 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 3aa54b20..cb1bcd15 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 21d7a5ac..fd7d8e71 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 68dbb1b1..78567b1a 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 c042591d..d155ac18 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 c0312ae7..62dc277c 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 e2653bc8..9d26c14a 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;
-- 
GitLab