Remove unused parameter from cpp_destructor and fix types

Author: tautschnig

src/cpp/cpp_destructor.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 /// \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);
     }

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

src/cpp/cpp_typecheck_destructor.cpp

@@ -134,13 +134,12 @@ 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.add_source_location() = source_location;
 
-    codet dtor_code=
-      cpp_destructor(source_location, cit->type(), member);
+    codet dtor_code = cpp_destructor(source_location, member);
 
     if(dtor_code.is_not_nil())
       block.move_to_operands(dtor_code);
@@ -158,14 +157,10 @@ 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());
+    dereference_exprt object(exprt("cpp-this"), psymb.type);
     object.add_source_location() = source_location;
 
-    exprt dtor_code =
-      cpp_destructor(source_location, psymb.type, object);
+    exprt dtor_code = cpp_destructor(source_location, object);
 
     if(dtor_code.is_not_nil())
       block.move_to_operands(dtor_code);

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