C++ type checking: use reference_typet, pointer_typet

Hoist type conversions up for improved type safety and clarity.

Author: tautschnig

src/cpp/cpp_typecheck.h

@@ -25,6 +25,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <set>
 #include <unordered_set>
 
+class pointer_typet;
+class reference_typet;
+
 bool cpp_typecheck(
   cpp_parse_treet &cpp_parse_tree,
   symbol_table_baset &symbol_table,
@@ -524,14 +527,18 @@ class cpp_typecheckt:public c_typecheck_baset
   bool user_defined_conversion_sequence(
     const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
 
-  bool reference_related(
-    const exprt &expr, const typet &type) const;
+  bool reference_related(const exprt &expr, const reference_typet &type) const;
 
   bool reference_compatible(
-    const exprt &expr, const typet &type, unsigned &rank) const;
+    const exprt &expr,
+    const reference_typet &type,
+    unsigned &rank) const;
 
   bool reference_binding(
-    exprt expr, const typet &type, exprt &new_expr, unsigned &rank);
+    exprt expr,
+    const reference_typet &type,
+    exprt &new_expr,
+    unsigned &rank);
 
   bool implicit_conversion_sequence(
     const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
@@ -542,7 +549,7 @@ class cpp_typecheckt:public c_typecheck_baset
   bool implicit_conversion_sequence(
     const exprt &expr, const typet &type, exprt &new_expr);
 
-  void reference_initializer(exprt &expr, const typet &type);
+  void reference_initializer(exprt &expr, const reference_typet &type);
 
   void implicit_typecast(exprt &expr, const typet &type) override;
 
@@ -556,9 +563,7 @@ class cpp_typecheckt:public c_typecheck_baset
     const struct_typet &from,
     const struct_typet &to) const;
 
-  void make_ptr_typecast(
-    exprt &expr,
-    const typet &dest_type);
+  void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type);
 
   // the C++ typecasts
 

src/cpp/cpp_typecheck_code.cpp

@@ -258,8 +258,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
     PRECONDITION(this_expr.is_not_nil());
 
     make_ptr_typecast(
-      this_expr,
-      code_type.parameters().front().type());
+      this_expr, to_pointer_type(code_type.parameters().front().type()));
 
     function_call.arguments().push_back(this_expr);
 
@@ -354,7 +353,8 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
           throw 0;
         }
 
-        reference_initializer(code.op0(), symbol_expr.type());
+        reference_initializer(
+          code.op0(), to_reference_type(symbol_expr.type()));
 
         // assign the pointers
         symbol_expr.type().remove(ID_C_reference);

src/cpp/cpp_typecheck_compound_type.cpp

@@ -1680,18 +1680,17 @@ bool cpp_typecheckt::subtype_typecast(
 
 void cpp_typecheckt::make_ptr_typecast(
   exprt &expr,
-  const typet &dest_type)
+  const pointer_typet &dest_type)
 {
   typet src_type=expr.type();
 
   PRECONDITION(src_type.id() == ID_pointer);
-  PRECONDITION(dest_type.id() == ID_pointer);
 
   const struct_typet &src_struct = to_struct_type(
     static_cast<const typet &>(follow(to_pointer_type(src_type).base_type())));
 
-  const struct_typet &dest_struct = to_struct_type(
-    static_cast<const typet &>(follow(to_pointer_type(dest_type).base_type())));
+  const struct_typet &dest_struct =
+    to_struct_type(static_cast<const typet &>(follow(dest_type.base_type())));
 
   PRECONDITION(
     subtype_typecast(src_struct, dest_struct) ||