diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 82d796b18aa..49704869ee8 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// \return typechecked code codet cpp_typecheckt::cpp_destructor( const source_locationt &source_location, - const typet &type, const exprt &object) { codet new_code; @@ -74,8 +73,7 @@ codet cpp_typecheckt::cpp_destructor( index_exprt index(object, constant); index.add_source_location()=source_location; - exprt i_code = - cpp_destructor(source_location, tmp_type.subtype(), index); + exprt i_code = cpp_destructor(source_location, index); new_code.move_to_operands(i_code); } @@ -119,29 +117,19 @@ codet cpp_typecheckt::cpp_destructor( cpp_name.get_sub().back().set(ID_identifier, dtor_name); cpp_name.get_sub().back().set(ID_C_source_location, source_location); + exprt member(ID_member); + member.add(ID_component_cpp_name) = cpp_name; + member.copy_to_operands(object); + side_effect_expr_function_callt function_call; function_call.add_source_location()=source_location; - function_call.function().swap(static_cast(cpp_name)); + function_call.function().swap(member); typecheck_side_effect_function_call(function_call); - assert(function_call.get(ID_statement)==ID_temporary_object); - - exprt &initializer = - static_cast(function_call.add(ID_initializer)); - - assert(initializer.id()==ID_code - && initializer.get(ID_statement)==ID_expression); - - side_effect_expr_function_callt &func_ini= - to_side_effect_expr_function_call(initializer.op0()); - - exprt &tmp_this=func_ini.arguments().front(); - assert(tmp_this.id()==ID_address_of - && tmp_this.op0().id()=="new_object"); - - tmp_this=address_of_exprt(object, pointer_type(object.type())); + already_typechecked(function_call); - new_code.swap(initializer); + new_code = code_expressiont(function_call); + new_code.add_source_location() = source_location; } return new_code; diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 596cde8a3a7..e7a74aed1ff 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -432,7 +432,6 @@ class cpp_typecheckt:public c_typecheck_baset codet cpp_destructor( const source_locationt &source_location, - const typet &type, const exprt &object); // expressions diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index e985f16b7de..193dede0a8f 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" +#include + bool cpp_typecheckt::find_dtor(const symbolt &symbol) const { const irept &components= @@ -134,13 +136,16 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) cpp_namet cppname; cppname.get_sub().push_back(name); - exprt member(ID_ptrmember); + exprt member(ID_ptrmember, type); member.set(ID_component_cpp_name, cppname); - member.operands().push_back(exprt("cpp-this")); + member.operands().push_back( + symbol_exprt(ID_this, pointer_type(symbol.type))); member.add_source_location() = source_location; - codet dtor_code= - cpp_destructor(source_location, cit->type(), member); + const bool disabled_access_control = disable_access_control; + disable_access_control = true; + codet dtor_code = cpp_destructor(source_location, member); + disable_access_control = disabled_access_control; if(dtor_code.is_not_nil()) block.move_to_operands(dtor_code); @@ -158,14 +163,14 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) assert(bit->find(ID_type).id()==ID_symbol); const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier)); - // TODO(tautschnig): object is not type checked before passing it to - // cpp_destructor even though cpp_destructor makes heavy use of the .type() - // member - dereference_exprt object(exprt("cpp-this"), nil_typet()); + symbol_exprt this_ptr(ID_this, pointer_type(symbol.type)); + dereference_exprt object(this_ptr, psymb.type); object.add_source_location() = source_location; - exprt dtor_code = - cpp_destructor(source_location, psymb.type, object); + const bool disabled_access_control = disable_access_control; + disable_access_control = true; + exprt dtor_code = cpp_destructor(source_location, object); + disable_access_control = disabled_access_control; if(dtor_code.is_not_nil()) block.move_to_operands(dtor_code); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 310407853a5..501baeeeb22 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1073,7 +1073,6 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr) codet destructor_code=cpp_destructor( expr.source_location(), - pointer_type.subtype(), new_object); // this isn't typechecked yet