Merge pull request diffblue#2269 from peterschrammel/parameters-code-…

…type

Make sure code_typet always has parameters property

jbmc/regression/jdiff/java-clinit-wrapper/test.desc

@@ -0,0 +1,8 @@
+CORE
+new.jar
+old.jar
+EXIT=0
+SIGNAL=0
+--
+java::java\.nio\.charset\.StandardCharsets::clinit_wrapper$
+java::org\.apache\.tika\.mime\.MediaType::clinit_wrapper$

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -760,15 +760,12 @@ 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_lang_object_type());
 
     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,11 +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();
-  // Ensure the parameters property is there
-  // to avoid trouble in irept comparisons
-  wrapper_method_type.parameters();
+  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";
@@ -717,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/java-testing-utils/module_dependencies.txt

@@ -0,0 +1,6 @@
+goto-programs
+java_bytecode
+java-testing-utils
+langapi # should go away
+testing-utils
+util

jbmc/unit/java_bytecode/ci_lazy_methods/module_dependencies.txt

@@ -0,0 +1,3 @@
+ci_lazy_methods
+java-testing-utils
+testing-utils

jbmc/unit/java_bytecode/goto-programs/module_dependencies.txt

@@ -0,0 +1,4 @@
+goto-programs
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/goto_program_generics/module_dependencies.txt

@@ -0,0 +1,4 @@
+goto_program_generics
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/inherited_static_fields/module_dependencies.txt

@@ -0,0 +1,4 @@
+inherited_static_fields
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt

@@ -1,3 +1,4 @@
 java-testing-utils
 testing-utils
 java_bytecode
+util

jbmc/unit/java_bytecode/java_bytecode_convert_method/module_dependencies.txt

@@ -0,0 +1,6 @@
+goto-programs
+java_bytecode
+java_bytecode_convert_method
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/java_bytecode_parse_generics/module_dependencies.txt

@@ -0,0 +1,3 @@
+java_bytecode_parse_generics
+java-testing-utils
+testing-utils

jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/module_dependencies.txt

@@ -0,0 +1,6 @@
+java_bytecode
+java_bytecode_parse_lambdas
+java-testing-utils
+langapi # should go away
+testing-utils
+util

jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt

@@ -0,0 +1,5 @@
+java_bytecode
+java_object_factory
+langapi # should go away
+testing-utils
+util

jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt

@@ -0,0 +1,7 @@
+goto-instrument
+goto-programs
+java_bytecode
+java_replace_nondet
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/java_string_library_preprocess/module_dependencies.txt

@@ -0,0 +1,5 @@
+java_bytecode
+java_string_library_preprocess
+langapi # should go away
+testing-utils
+util

jbmc/unit/java_bytecode/java_types/module_dependencies.txt

@@ -0,0 +1,3 @@
+java_bytecode
+java_types
+testing-utils

jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt

@@ -0,0 +1,7 @@
+goto-instrument
+goto-programs
+java_bytecode
+java_virtual_functions
+java-testing-utils
+testing-utils
+util

jbmc/unit/java_bytecode/module_dependencies.txt

@@ -0,0 +1,2 @@
+java_bytecode
+testing-utils

jbmc/unit/pointer-analysis/module_dependencies.txt

@@ -0,0 +1,6 @@
+goto-programs
+java_bytecode
+langapi # should go away
+pointer-analysis
+testing-utils
+util

jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt

@@ -0,0 +1,7 @@
+java_bytecode
+langapi # should go away
+solvers/refinement
+solvers/sat
+string_constraint_instantiation
+testing-utils
+util

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

@@ -58,7 +58,12 @@ 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(
+      {code_typet::parametert(length_type()),
+       code_typet::parametert(pointer_type(java_char_type())),
+       code_typet::parametert(string_type),
+       code_typet::parametert(string_type)},
+      unsignedbv_typet(32));
 
     // fun1 is s3 = s1.concat(s2)
     function_application_exprt fun1(fun_type);

jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt

@@ -0,0 +1,6 @@
+java_bytecode
+langapi # should go away
+string_refinement
+solvers/refinement
+testing-utils
+util

jbmc/unit/util/module_dependencies.txt

@@ -0,0 +1,4 @@
+java_bytecode
+java-testing-utils
+testing-utils
+util

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/cbmc/symex_coverage.cpp

@@ -173,8 +173,6 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
 
   code_typet sig_type=
     original_return_type(ns.get_symbol_table(), gf_it->first);
-  if(sig_type.is_nil())
-    sig_type=gf_it->second.type;
   xml.set_attribute("signature",
                     from_type(ns, gf_it->first, sig_type));