Merge pull request #2269 from peterschrammel/parameters-code-type

Make sure code_typet always has parameters property

Author: kroening

jbmc/regression/jdiff/java-clinit-wrapper/new.jar

@@ -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/regression/jdiff/java-clinit-wrapper/old.jar

@@ -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/regression/jdiff/java-clinit-wrapper/test.desc

@@ -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_bytecode_convert_class.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_entry_point.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_static_initializers.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/src/java_bytecode/java_string_library_preprocess.cpp

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

jbmc/src/java_bytecode/java_types.cpp

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