diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 9a1866bedf5..7ce819fbbbc 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/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
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 24f515685e5..146e4f5a0e2 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/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;