Set declaring class for string solver implemented methods

The declaring class was not previously set for methods which are
implemented by the string solver. This commit sets the declaring class
for the initially empty valued method symbols. INVARIANTs are used to
check that the declaring class is still set once the value of the symbol
has been provided for the methods implemented by the string solver. The
non violation of this INVARIANT is tested by all `strings-smoke-tests`
which call such methods. For example the tests in
`regression/strings-smoke-tests/java_int_to_string` will check that the
INVARIANT holds for `Integer.toString`.

Author: thomasspriggs

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -388,6 +388,7 @@ void java_bytecode_convert_method_lazy(
   // Not used in jbmc at present, but other codebases that use jbmc as a library
   // use this information.
   method_symbol.type.set(ID_C_abstract, m.is_abstract);
+  set_declaring_class(method_symbol, class_symbol.name);
 
   if(java_bytecode_parse_treet::find_annotation(
        m.annotations, "java::org.cprover.MustNotThrow"))

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1033,6 +1033,7 @@ bool java_bytecode_languaget::convert_single_method(
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
 {
   const symbolt &symbol = symbol_table.lookup_ref(function_id);
+  INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
 
   // Nothing to do if body is already loaded
   if(symbol.value.is_not_nil())
@@ -1060,6 +1061,8 @@ bool java_bytecode_languaget::convert_single_method(
     // Add these to the needed_lazy_methods collection
     notify_static_method_calls(generated_code, needed_lazy_methods);
     writable_symbol.value = std::move(generated_code);
+    INVARIANT(
+      declaring_class(writable_symbol), "Method must have a declaring class.");
     return false;
   }
   else if(