Merge pull request #4502 from tautschnig/parameter-names

Ensure Java stubbing names parameters [blocks: #4485]

Author: tautschnig

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -148,12 +148,29 @@ void java_simple_method_stubst::create_method_stub_at(
 void java_simple_method_stubst::create_method_stub(symbolt &symbol)
 {
   code_blockt new_instructions;
-  const java_method_typet &required_type = to_java_method_type(symbol.type);
+  java_method_typet &required_type = to_java_method_type(symbol.type);
 
   // synthetic source location that contains the opaque function name only
   source_locationt synthesized_source_location;
   synthesized_source_location.set_function(symbol.name);
 
+  // make sure all parameters are named
+  for(auto &parameter : required_type.parameters())
+  {
+    if(parameter.get_identifier().empty())
+    {
+      symbolt &parameter_symbol = fresh_java_symbol(
+        parameter.type(),
+        "#anon",
+        synthesized_source_location,
+        symbol.name,
+        symbol_table);
+      parameter_symbol.is_parameter = true;
+      parameter.set_base_name(parameter_symbol.base_name);
+      parameter.set_identifier(parameter_symbol.name);
+    }
+  }
+
   // Initialize the return value or `this` parameter under construction.
   // Note symbol.type is required_type, but with write access
   // Probably required_type should not be const

src/goto-programs/goto_convert_functions.cpp

@@ -159,6 +159,15 @@ void goto_convert_functionst::convert_function(
      symbol.is_compiled()) /* goto_inline may have removed the body */
     return;
 
+  // we have a body, make sure all parameter names are valid
+  for(const auto &p : f.parameter_identifiers)
+  {
+    DATA_INVARIANT(!p.empty(), "parameter identifier should not be empty");
+    DATA_INVARIANT(
+      symbol_table.has_symbol(p),
+      "parameter identifier must be a known symbol");
+  }
+
   lifetimet parent_lifetime = lifetime;
   lifetime = identifier == INITIALIZE_FUNCTION ? lifetimet::STATIC_GLOBAL
                                                : lifetimet::AUTOMATIC_LOCAL;