diff --git a/convert.ml b/convert.ml index d0d4938c7ee25ad863343a5826cf57f72dd954e1..3aae9f5de0f77a849252ace41523709ba1fdf992 100644 --- a/convert.ml +++ b/convert.ml @@ -2710,8 +2710,71 @@ let extract_decl = function has_further_definition,None,None) | c -> c +let implicit_kind = function + | CMethod(_,_,kind,_,args,_,_,_,_,_,_,_) -> + (match kind, args with + | FKConstructor false, [_] -> 1 (* default constructor, plain. *) + | FKConstructor true, [_] -> 2 (* default constructor, derived. *) + | FKConstructor false, + [_; { arg_type = { plain_type = LVReference _; qualifier }}] + when List.mem Const qualifier -> 3 (* copy constructor, const, plain. *) + | FKConstructor false, + [_; { arg_type = { plain_type = LVReference _; }}] -> + (* copy constructor, non-const, plain. *) + 4 + | FKConstructor true, + [_; { arg_type = { plain_type = LVReference _; qualifier }}] + when List.mem Const qualifier -> 5 (* copy constructor, const,derived. *) + | FKConstructor true, + [_; { arg_type = { plain_type = LVReference _; }}] -> + (* copy constructor, non-const, derived. *) + 6 + | FKConstructor false, + [_; { arg_type = { plain_type = RVReference _; qualifier }}] + when List.mem Const qualifier -> 7 (* move constructor, const, plain. *) + | FKConstructor false, + [_; { arg_type = { plain_type = RVReference _; }}] -> + (* move constructor, non-const, plain. *) + 8 + | FKConstructor true, + [_; { arg_type = { plain_type = RVReference _; qualifier }}] + when List.mem Const qualifier -> 9 (* move constructor, const,derived. *) + | FKConstructor true, + [_; { arg_type = { plain_type = RVReference _; }}] -> + (* move constructor, non-const, derived. *) + 10 + | FKMethod _, + [ _; { arg_type = { plain_type = (Struct _ | Union _); qualifier } }] + when List.mem Const qualifier -> 11 (*assign operator, const *) + | FKMethod _, + [ _; { arg_type = { plain_type = (Struct _ | Union _); } }] -> + 12 (*assign operator, non const *) + | FKMethod _, + [ _; { arg_type = { plain_type = LVReference _; qualifier } }] + when List.mem Const qualifier -> 13 (* assign operator, const *) + | FKMethod _, + [ _; { arg_type = { plain_type = LVReference _; } }] -> + 14 (* assign operator, non-const *) + | FKMethod _, + [ _; { arg_type = { plain_type = RVReference _; qualifier } }] + when List.mem Const qualifier -> 15 (* move operator, const *) + | FKMethod _, + [ _; { arg_type = { plain_type = RVReference _; } }] -> + 16 (* move operator, non-const *) + | FKDestructor false, [ _ ] -> 17 (* destructor, plain. *) + | FKDestructor true, [ _ ] -> 18 (* destructor, derived. *) + | _ -> 0 (* unknown implicit operator, don't try to sort it. *) + ) + | _ -> 0 (* unknown declaration, don't try to sort it. *) + +let cmp_implicit i1 i2 = + let n1 = implicit_kind i1 in + let n2 = implicit_kind i2 in + compare n1 n2 + let reorder_implicit l = let implicit = Extlib.filter_map is_implicit_func extract_decl l in + let implicit = List.stable_sort cmp_implicit implicit in implicit @ l let iter_on_array ?(incr=true) env idx length mk_body = diff --git a/tests/basic/oracle/c_link.res.oracle b/tests/basic/oracle/c_link.res.oracle index 9629c48bfd1deea3d7e63ac93fabe266f2a543ef..cdd0578f1d993f6d1fd4a69fc1e392170a441d38 100644 --- a/tests/basic/oracle/c_link.res.oracle +++ b/tests/basic/oracle/c_link.res.oracle @@ -35,10 +35,10 @@ struct Bar { }; void Foo::Ctor(struct Foo const *this); -void Foo::Dtor(struct Foo const *this); - struct Foo *operator=(struct Foo *this, struct Foo *__frama_c_arg_0); +void Foo::Dtor(struct Foo const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/basic/oracle/pointer_to_member.res.oracle b/tests/basic/oracle/pointer_to_member.res.oracle index ae4e52041be8d1f3e654eb9436e7c9a4095181d5..c05062e31860af5d35b9f78f76b25f4bfa7524ce 100644 --- a/tests/basic/oracle/pointer_to_member.res.oracle +++ b/tests/basic/oracle/pointer_to_member.res.oracle @@ -33,10 +33,10 @@ struct Bar { static int g = 0; void f(int i); -void Foo::Dtor(struct Foo const *this); - void Foo::Ctor(struct Foo const *this); +void Foo::Dtor(struct Foo const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; @@ -289,10 +289,10 @@ struct _frama_c_vmt _frama_c_vmt_header = {.table = _frama_c_vmt, .table_size = 1, .rtti_info = & _frama_c_rtti_name_info}; -void Bar::Dtor(struct Bar const *this); - void Bar::Ctor(struct Bar const *this); +void Bar::Dtor(struct Bar const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/basic/oracle/pointer_to_virtual_method.res.oracle b/tests/basic/oracle/pointer_to_virtual_method.res.oracle index ab9b97e1eb0bee7cb72c5ff33ec8497c6c2e9ab4..56e749cb781bf252cb4b86f351f9df949b20f176 100644 --- a/tests/basic/oracle/pointer_to_virtual_method.res.oracle +++ b/tests/basic/oracle/pointer_to_virtual_method.res.oracle @@ -31,10 +31,10 @@ struct Bar { struct Foo _frama_c__Z3Foo ; }; static int g = 0; -void Foo::Dtor(struct Foo const *this); - void Foo::Ctor(struct Foo const *this); +void Foo::Dtor(struct Foo const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; @@ -287,10 +287,10 @@ struct _frama_c_vmt _frama_c_vmt_header = {.table = _frama_c_vmt, .table_size = 1, .rtti_info = & _frama_c_rtti_name_info}; -void Bar::Dtor(struct Bar const *this); - void Bar::Ctor(struct Bar const *this); +void Bar::Dtor(struct Bar const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/class/oracle/constr.res.oracle b/tests/class/oracle/constr.res.oracle index be2afc344e2c5e20d5333fc130d0a67cef57c372..8e5eda82c40e982ddd0964a70317dc243a802c7d 100644 --- a/tests/class/oracle/constr.res.oracle +++ b/tests/class/oracle/constr.res.oracle @@ -26,10 +26,10 @@ struct Foo; struct Foo { int x ; }; -void Foo::Dtor(struct Foo const *this); - struct Foo *operator=(struct Foo *this, struct Foo *__frama_c_arg_0); +void Foo::Dtor(struct Foo const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/class/oracle/inheritance_out_def.res.oracle b/tests/class/oracle/inheritance_out_def.res.oracle index 96f87f64b9d5527a0080f952a9dc9514eacb7b67..c8a22ff4c9abba325131da43222c3286513c53e7 100644 --- a/tests/class/oracle/inheritance_out_def.res.oracle +++ b/tests/class/oracle/inheritance_out_def.res.oracle @@ -32,10 +32,10 @@ struct B { struct A _frama_c__Z1A ; int y ; }; -void A::Dtor(struct A const *this); - void A::Ctor(struct A const *this); +void A::Dtor(struct A const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle index cec683ab6e30d3f51ec91a9ef6edd2fa78781443..3aa54b20c452e6755f0fe246cec438b891e24943 100644 --- a/tests/stl/oracle/stl_algorithm.res.oracle +++ b/tests/stl/oracle/stl_algorithm.res.oracle @@ -2217,11 +2217,11 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .pvmt = (struct _frama_c_vmt *)0}; void __bool_binop<int,std::__equal_to>::Ctor(struct __bool_binop<int,std::__equal_to> const *this); -void __bool_binop<int,std::__equal_to>::Dtor(struct __bool_binop<int,std::__equal_to> const *this); - void __bool_binop<int,std::__equal_to>::Ctor(struct __bool_binop<int,std::__equal_to> const *this, struct __bool_binop<int,std::__equal_to> const *__frama_c_arg_0); +void __bool_binop<int,std::__equal_to>::Dtor(struct __bool_binop<int,std::__equal_to> const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle index c4935b3f3169ae3a792c3db269d627d3cf12412e..21d7a5ac23f49d50873cec5944fa19f3c036f2a0 100644 --- a/tests/stl/oracle/stl_functional.res.oracle +++ b/tests/stl/oracle/stl_functional.res.oracle @@ -1979,11 +1979,11 @@ struct reference_wrapper<int*,<abst>> ref<int*,<abst>>(int (**t)(int )) void __binop<int,std::__minus>::Ctor(struct __binop<int,std::__minus> const *this); -void __binop<int,std::__minus>::Dtor(struct __binop<int,std::__minus> const *this); - void __binop<int,std::__minus>::Ctor(struct __binop<int,std::__minus> const *this, struct __binop<int,std::__minus> *__frama_c_arg_0); +void __binop<int,std::__minus>::Dtor(struct __binop<int,std::__minus> const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; @@ -2026,11 +2026,11 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .pvmt = (struct _frama_c_vmt *)0}; void __binop<int,std::__plus>::Ctor(struct __binop<int,std::__plus> const *this); -void __binop<int,std::__plus>::Dtor(struct __binop<int,std::__plus> const *this); - void __binop<int,std::__plus>::Ctor(struct __binop<int,std::__plus> const *this, struct __binop<int,std::__plus> *__frama_c_arg_0); +void __binop<int,std::__plus>::Dtor(struct __binop<int,std::__plus> const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_iterator.res.oracle b/tests/stl/oracle/stl_iterator.res.oracle index b97d9660dc973fbe0a4bb13325ae8a0b947d341d..68dbb1b1d9c26f30d962cc1e88240bf8e8035ff9 100644 --- a/tests/stl/oracle/stl_iterator.res.oracle +++ b/tests/stl/oracle/stl_iterator.res.oracle @@ -321,14 +321,14 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .base_classes = (struct _frama_c_rtti_name_info_content *)0, .number_of_base_classes = 0, .pvmt = (struct _frama_c_vmt *)0}; -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); 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, struct iterator<std::random_access_iterator_tag,int,int,int*,int&> const *__frama_c_arg_0); -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); struct _frama_c_vmt _frama_c_vmt_header; @@ -365,11 +365,11 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .base_classes = (struct _frama_c_rtti_name_info_content *)0, .number_of_base_classes = 0, .pvmt = (struct _frama_c_vmt *)0}; -void reverse_iterator<int*>::Dtor(struct reverse_iterator<int*> const *this); - void reverse_iterator<int*>::Ctor(struct reverse_iterator<int*> const *this, struct reverse_iterator<int*> const *__frama_c_arg_0); +void reverse_iterator<int*>::Dtor(struct reverse_iterator<int*> const *this); + struct _frama_c_vmt _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle index 9459d839ac65d11470634fe9ee59a7e912fffa11..c042591d8edbfc2968e99f54b2b05e6bb34e6f6d 100644 --- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle +++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle @@ -1816,10 +1816,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .base_classes = (struct _frama_c_rtti_name_info_content *)0, .number_of_base_classes = 0, .pvmt = (struct _frama_c_vmt *)0}; -void __shared_ref_base::Dtor(struct __shared_ref_base const *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 _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle index f2db83c2f9074826407a9020ff6952219eb51bf5..c0312ae75ac14203b6c0b263a7bd308490963565 100644 --- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle +++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle @@ -1774,10 +1774,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .base_classes = (struct _frama_c_rtti_name_info_content *)0, .number_of_base_classes = 0, .pvmt = (struct _frama_c_vmt *)0}; -void __shared_ref_base::Dtor(struct __shared_ref_base const *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 _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle index 5e6fbbc1e378b9b362ee0957771425c7ee17c20f..e2653bc827f44c07694449142110470c57e38928 100644 --- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle +++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle @@ -1780,10 +1780,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = .base_classes = (struct _frama_c_rtti_name_info_content *)0, .number_of_base_classes = 0, .pvmt = (struct _frama_c_vmt *)0}; -void __shared_ref_base::Dtor(struct __shared_ref_base const *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 _frama_c_vmt_header; struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;