Ensure Java stubbing names parameters [blocks: #4485]

[tautschnig]

For functions with a body we require that parameters are named so that
we can generate assignments to them (even when the body may not read the
value). Also guard against future regressions by sanity checking
parameter names for any converted function.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[smowton]

Got to this late, but this should be done when assign_parameter_names is called when a stub function is created in java_bytecode_convert_method.cpp, do you have any idea why that wasn't happening in your case (or should that call be removed now?) Could you submit a followup with whatever test case motivated this?

[tautschnig]

It's jbmc/provide_object_implementation/ that fails without the patch (but the additional sanity check kept in). assign_parameter_names is never called for the symbol at fault (java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;), which gets added into the symbol table in typecheck_expr_symbol. Note that this test uses --no-lazy-methods, which may be important here (I don't think the method at fault is ever invoked, and assign_parameter_names is AFAIK only called for invoked methods).

So I accept that maybe some other place is the right one to fix this, but I don't really have a sufficiently good understanding of the Java front-end to make that change.