Merge pull request #3006 from tautschnig/return-type

Access code_typet::return_type() via code_typet's API

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -927,8 +927,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
 
     code_function_callt &fc=to_code_function_call(last);
 
-    auto return_type =
-      static_cast<const typet &>(fc.function().type().find(ID_return_type));
+    const auto &return_type = to_code_type(fc.function().type()).return_type();
 
     side_effect_expr_function_callt sideeffect(
       fc.function(), fc.arguments(), return_type, fc.source_location());
@@ -1997,9 +1996,8 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         new_symbol.name=identifier;
         new_symbol.base_name=identifier;
         new_symbol.location=expr.source_location();
-        new_symbol.type=code_typet();
+        new_symbol.type = code_typet({}, return_type);
         new_symbol.type.set(ID_C_incomplete, true);
-        new_symbol.type.add(ID_return_type)=return_type;
 
         // TODO: should also guess some argument types
 

src/cpp/cpp_constructor.cpp

@@ -218,7 +218,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
 
       if(
         !c.get_bool(ID_from_base) && type.id() == ID_code &&
-        type.find(ID_return_type).id() == ID_constructor)
+        to_code_type(type).return_type().id() == ID_constructor)
       {
         constructor_name = c.get(ID_base_name);
         break;

src/cpp/cpp_convert_type.cpp

@@ -220,12 +220,12 @@ void cpp_convert_typet::read_template(const typet &type)
 void cpp_convert_typet::read_function_type(const typet &type)
 {
   other.push_back(type);
-  typet &t=other.back();
-  t.id(ID_code);
+  other.back().id(ID_code);
+
+  code_typet &t = to_code_type(other.back());
 
   // change subtype to return_type
-  typet &return_type=
-    static_cast<typet &>(t.add(ID_return_type));
+  typet &return_type = t.return_type();
 
   return_type.swap(t.subtype());
   t.remove_subtype();

src/cpp/cpp_declarator_converter.cpp

@@ -131,7 +131,7 @@ symbolt &cpp_declarator_convertert::convert(
 
     // If it is a constructor, we take care of the
     // object initialization
-    if(final_type.get(ID_return_type)==ID_constructor)
+    if(to_code_type(final_type).return_type().id() == ID_constructor)
     {
       const cpp_namet &name=declarator.name();
 
@@ -326,11 +326,10 @@ void cpp_declarator_convertert::handle_initializer(
 {
   exprt &value=declarator.value();
 
-  // moves member initializers into 'value'
-  cpp_typecheck.move_member_initializers(
-    declarator.member_initializers(),
-    symbol.type,
-    value);
+  // moves member initializers into 'value' - only methods have these
+  if(symbol.type.id() == ID_code)
+    cpp_typecheck.move_member_initializers(
+      declarator.member_initializers(), to_code_type(symbol.type), value);
 
   // any initializer to be done?
   if(value.is_nil())

src/cpp/cpp_destructor.cpp

@@ -92,7 +92,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
 
       if(
         !c.get_bool(ID_from_base) && type.id() == ID_code &&
-        type.find(ID_return_type).id() == ID_destructor)
+        to_code_type(type).return_type().id() == ID_destructor)
       {
         dtor_name = c.get(ID_base_name);
         break;

src/cpp/cpp_typecheck.cpp

@@ -207,8 +207,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
   init_symbol.value.swap(init_block);
   init_symbol.mode=ID_cpp;
   init_symbol.module=module;
-  init_symbol.type=code_typet();
-  init_symbol.type.add(ID_return_type)=typet(ID_constructor);
+  init_symbol.type = code_typet({}, typet(ID_constructor));
   init_symbol.is_type=false;
   init_symbol.is_macro=false;
 

src/cpp/cpp_typecheck.h

@@ -387,7 +387,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void move_member_initializers(
     irept &initializers,
-    const typet &type,
+    const code_typet &type,
     exprt &value);
 
   static bool has_const(const typet &type);

src/cpp/cpp_typecheck_compound_type.cpp

@@ -490,7 +490,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
     if(has_volatile(method_qualifier))
       virtual_name += "$volatile";
 
-    if(component.type().get(ID_return_type)==ID_destructor)
+    if(to_code_type(component.type()).return_type().id() == ID_destructor)
       virtual_name="@dtor";
 
     // The method may be virtual implicitly.
@@ -802,7 +802,7 @@ void cpp_typecheckt::put_compound_into_scope(
     id.class_identifier=cpp_scopes.current_scope().identifier;
     id.is_member=true;
     id.is_constructor =
-      compound.find(ID_type).get(ID_return_type)==ID_constructor;
+      to_code_type(compound.type()).return_type().id() == ID_constructor;
     id.is_method=true;
     id.is_static_member=compound.get_bool(ID_is_static);
 
@@ -1226,20 +1226,17 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
 
 void cpp_typecheckt::move_member_initializers(
   irept &initializers,
-  const typet &type,
+  const code_typet &type,
   exprt &value)
 {
-  bool is_constructor=
-    type.find(ID_return_type).id()==ID_constructor;
-
   // see if we have initializers
   if(!initializers.get_sub().empty())
   {
     const source_locationt &location=
       static_cast<const source_locationt &>(
         initializers.find(ID_C_source_location));
 
-    if(!is_constructor)
+    if(type.return_type().id() != ID_constructor)
     {
       error().source_location=location;
       error() << "only constructors are allowed to "
@@ -1275,7 +1272,7 @@ void cpp_typecheckt::typecheck_member_function(
 {
   symbolt symbol;
 
-  typet &type=component.type();
+  code_typet &type = to_code_type(component.type());
 
   if(component.get_bool(ID_is_static))
   {

src/cpp/cpp_typecheck_constructor.cpp

@@ -603,8 +603,8 @@ void cpp_typecheckt::check_member_initializers(
       // Parent constructor
       if(
         c.get_bool(ID_from_base) && !c.get_bool(ID_is_type) &&
-        !c.get_bool(ID_is_static) && c.get(ID_type) == ID_code &&
-        c.find(ID_type).get(ID_return_type) == ID_constructor)
+        !c.get_bool(ID_is_static) && c.type().id() == ID_code &&
+        to_code_type(c.type()).return_type().id() == ID_constructor)
       {
         typet member_type=(typet&) initializer.find(ID_member);
         typecheck_type(member_type);

src/cpp/cpp_typecheck_conversions.cpp

@@ -927,7 +927,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
         if(comp_type.id() !=ID_code)
           continue;
 
-        if(comp_type.find(ID_return_type).id() !=ID_constructor)
+        if(to_code_type(comp_type).return_type().id() != ID_constructor)
           continue;
 
         // TODO: ellipsis

src/cpp/cpp_typecheck_expr.cpp

@@ -1178,8 +1178,9 @@ void cpp_typecheckt::typecheck_expr_member(
 
     if(symbol_expr.id()==ID_symbol)
     {
-      if(symbol_expr.type().id()==ID_code &&
-         symbol_expr.type().get(ID_return_type)==ID_constructor)
+      if(
+        symbol_expr.type().id() == ID_code &&
+        to_code_type(symbol_expr.type()).return_type().id() == ID_constructor)
       {
         error().source_location=expr.find_source_location();
         error() << "error: member `"
@@ -1866,7 +1867,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
     if(symbol_expr.operands().empty() ||
        symbol_expr.op0().is_nil())
     {
-      if(symbol_expr.type().get(ID_return_type)!=ID_constructor)
+      if(to_code_type(symbol_expr.type()).return_type().id() != ID_constructor)
       {
         if(cpp_scopes.current_scope().this_expr.is_nil())
         {
@@ -2201,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
         if(
           !c.get_bool(ID_from_base) && type.id() == ID_code &&
-          type.find(ID_return_type).id() == ID_destructor)
+          to_code_type(type).return_type().id() == ID_destructor)
         {
           add_method_body(&symbol_table.get_writeable_ref(c.get(ID_name)));
           break;

src/cpp/cpp_typecheck_function.cpp

@@ -91,7 +91,7 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     return;
 
   // if it is a destructor, add the implicit code
-  if(symbol.type.get(ID_return_type)==ID_destructor)
+  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
   {
     const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
 

src/cpp/cpp_typecheck_resolve.cpp

@@ -655,7 +655,9 @@ void cpp_typecheck_resolvet::make_constructors(
         if(component.get_bool(ID_from_base))
           continue;
 
-        if(type.find(ID_return_type).id()==ID_constructor)
+        if(
+          type.id() == ID_code &&
+          to_code_type(type).return_type().id() == ID_constructor)
         {
           const symbolt &symb =
             cpp_typecheck.lookup(component.get_name());

src/cpp/template_map.cpp

@@ -50,7 +50,7 @@ void template_mapt::apply(typet &type) const
   }
   else if(type.id()==ID_code)
   {
-    apply(static_cast<typet &>(type.add(ID_return_type)));
+    apply(to_code_type(type).return_type());
 
     irept::subt &parameters=type.add(ID_parameters).get_sub();
 

src/goto-programs/builtin_functions.cpp

@@ -192,8 +192,7 @@ void goto_convertt::do_printf(
   if(f_id==CPROVER_PREFIX "printf" ||
      f_id=="printf")
   {
-    typet return_type=
-      static_cast<const typet &>(function.type().find(ID_return_type));
+    const typet &return_type = to_code_type(function.type()).return_type();
     side_effect_exprt printf_code(
       ID_printf, return_type, function.source_location());