Use the two-param code_typet constructor

Author: peterschrammel

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -760,15 +760,14 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     const irep_idt clone_name=
       id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
-    code_typet clone_type;
-    clone_type.return_type()=
-      java_reference_type(symbol_typet("java::java.lang.Object"));
     code_typet::parametert this_param;
     this_param.set_identifier(id2string(clone_name)+"::this");
     this_param.set_base_name("this");
     this_param.set_this();
     this_param.type()=java_reference_type(symbol_type);
-    clone_type.parameters().push_back(this_param);
+    code_typet clone_type(
+      {this_param},
+      java_reference_type(symbol_typet("java::java.lang.Object")));
 
     parameter_symbolt this_symbol;
     this_symbol.name=this_param.get_identifier();

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -31,8 +31,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  code_typet type;
-  type.return_type()=empty_typet();
+  code_typet type({}, empty_typet());
   initialize.type=type;
 
   code_blockt init_code;
@@ -688,8 +687,7 @@ bool generate_java_start_function(
   // we just built and register it in the symbol table
   symbolt new_symbol;
 
-  code_typet main_type;
-  main_type.return_type()=empty_typet();
+  code_typet main_type({}, empty_typet());
 
   new_symbol.name=goto_functionst::entry_point();
   new_symbol.type.swap(main_type);

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -293,8 +293,7 @@ static void create_clinit_wrapper_symbols(
 
   // Create symbol for the "clinit_wrapper"
   symbolt wrapper_method_symbol;
-  code_typet wrapper_method_type;
-  wrapper_method_type.return_type() = void_typet();
+  code_typet wrapper_method_type({}, void_typet());
   wrapper_method_symbol.name = clinit_wrapper_name(class_name);
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -714,8 +713,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    code_typet thunk_type;
-    thunk_type.return_type() = void_typet();
+    code_typet thunk_type({}, void_typet());
 
     symbolt static_init_symbol;
     static_init_symbol.name = static_init_name;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1611,9 +1611,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
     "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
   fun_call.lhs()=class1;
   fun_call.arguments().push_back(string1);
-  code_typet fun_type;
-  fun_type.parameters().push_back(code_typet::parametert(string_ptr_type));
-  fun_type.return_type()=class_type;
+  code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
   fun_call.function().type()=fun_type;
   code.add(fun_call, loc);
 

jbmc/src/java_bytecode/java_types.cpp

@@ -493,24 +493,21 @@ typet java_type_from_string(
       if(e_pos==std::string::npos)
         return nil_typet();
 
-      code_typet result;
-
-      result.return_type()=
-        java_type_from_string(
-          std::string(src, e_pos+1, std::string::npos),
-          class_name_prefix);
+      typet return_type = java_type_from_string(
+        std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
 
       std::vector<typet> param_types =
         parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
 
       // create parameters for each type
+      code_typet::parameterst parameters;
       std::transform(
         param_types.begin(),
         param_types.end(),
-        std::back_inserter(result.parameters()),
+        std::back_inserter(parameters),
         [](const typet &type) { return code_typet::parametert(type); });
 
-      return result;
+      return code_typet(std::move(parameters), std::move(return_type));
     }
 
   case '[': // array type

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

@@ -58,7 +58,9 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
     const symbol_exprt lhs("lhs", unsignedbv_typet(32));
     const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
     const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
-    code_typet fun_type;
+    code_typet fun_type(
+      {length_type(), pointer_type(java_char_type()), string_type, string_type},
+      unsignedbv_typet(32));
 
     // fun1 is s3 = s1.concat(s2)
     function_application_exprt fun1(fun_type);

src/ansi-c/ansi_c_entry_point.cpp

@@ -445,8 +445,7 @@ bool generate_ansi_c_start_function(
   // add the entry point symbol
   symbolt new_symbol;
 
-  code_typet main_type;
-  main_type.return_type()=empty_typet();
+  code_typet main_type({}, empty_typet());
 
   new_symbol.name=goto_functionst::entry_point();
   new_symbol.type.swap(main_type);

src/ansi-c/c_typecheck_expr.cpp

@@ -450,10 +450,8 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   typet arg_type=expr.type();
   typecheck_type(arg_type);
 
-  code_typet new_type;
-  new_type.return_type().swap(arg_type);
-  new_type.parameters().resize(1);
-  new_type.parameters()[0].type()=pointer_type(void_type());
+  code_typet new_type(
+    {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
 
   assert(expr.operands().size()==1);
   exprt arg=expr.op0();

src/cpp/cpp_typecheck_expr.cpp

@@ -1446,10 +1446,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      t.return_type()=ptr_arg.type().subtype();
       result.type()=t;
       expr.swap(result);
       return;
@@ -1480,10 +1479,10 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=ptr_arg.type().subtype();
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(signed_int_type())},
+        ptr_arg.type().subtype());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1514,12 +1513,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(
-        code_typet::parametert(ptr_arg.type().subtype()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=empty_typet();
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(ptr_arg.type().subtype()),
+         code_typet::parametert(signed_int_type())},
+        empty_typet());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1550,12 +1548,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(
-        code_typet::parametert(ptr_arg.type().subtype()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=ptr_arg.type().subtype();
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(ptr_arg.type().subtype()),
+         code_typet::parametert(signed_int_type())},
+        ptr_arg.type().subtype());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1594,11 +1591,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=empty_typet();
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(signed_int_type())},
+        empty_typet());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1643,12 +1640,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=empty_typet();
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(ptr_arg.type()),
+         code_typet::parametert(signed_int_type())},
+        empty_typet());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1698,20 +1695,19 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
+      code_typet::parameterst parameters;
+      parameters.push_back(code_typet::parametert(ptr_arg.type()));
+      parameters.push_back(code_typet::parametert(ptr_arg.type()));
 
       if(identifier=="__atomic_compare_exchange")
-        t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
+        parameters.push_back(code_typet::parametert(ptr_arg.type()));
       else
-        t.parameters().push_back(
-          code_typet::parametert(ptr_arg.type().subtype()));
+        parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));
 
-      t.parameters().push_back(code_typet::parametert(c_bool_type()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.parameters().push_back(code_typet::parametert(signed_int_type()));
-      t.return_type()=c_bool_type();
+      parameters.push_back(code_typet::parametert(c_bool_type()));
+      parameters.push_back(code_typet::parametert(signed_int_type()));
+      parameters.push_back(code_typet::parametert(signed_int_type()));
+      code_typet t(std::move(parameters), c_bool_type());
       result.type()=t;
       expr.swap(result);
       return;
@@ -1744,10 +1740,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      t.return_type()=ptr_arg.type().subtype();
       result.type()=t;
       expr.swap(result);
       return;
@@ -1780,10 +1775,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
       symbol_exprt result;
       result.add_source_location()=source_location;
       result.set_identifier(identifier);
-      code_typet t;
-      t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
+      code_typet t(
+        {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
       t.make_ellipsis();
-      t.return_type()=ptr_arg.type().subtype();
       result.type()=t;
       expr.swap(result);
       return;

src/cpp/cpp_typecheck_resolve.cpp

@@ -611,29 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(
 
       // 1. no arguments, default initialization
       {
-        code_typet t1;
-        t1.return_type()=it->type();
+        code_typet t1({}, it->type());
         exprt pod_constructor1("pod_constructor", t1);
         new_identifiers.push_back(pod_constructor1);
       }
 
       // 2. one argument, copy/conversion
       {
-        code_typet t2;
-        t2.return_type()=it->type();
-        t2.parameters().resize(1);
-        t2.parameters()[0].type()=it->type();
+        code_typet t2({code_typet::parametert(it->type())}, it->type());
         exprt pod_constructor2("pod_constructor", t2);
         new_identifiers.push_back(pod_constructor2);
       }
 
       // enums, in addition, can also be constructed from int
       if(symbol_type.id()==ID_c_enum_tag)
       {
-        code_typet t3;
-        t3.return_type()=it->type();
-        t3.parameters().resize(1);
-        t3.parameters()[0].type()=signed_int_type();
+        code_typet t3({code_typet::parametert(it->type())}, signed_int_type());
         exprt pod_constructor3("pod_constructor", t3);
         new_identifiers.push_back(pod_constructor3);
       }