Split add_array_type, specialize for enums

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2238,7 +2238,7 @@ void java_bytecode_convert_methodt::convert_invoke(
   if(is_enum_values_clone_call)
   {
     const std::string clone_name =
-      "java::array[" + calling_class_name + "].clone:()Ljava/lang/Object;";
+      "java::array[" + class_type_name + "].clone:()Ljava/lang/Object;";
     call.function() = symbol_exprt(clone_name, arg0.type());
   }
   else if(is_virtual)

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -653,6 +653,9 @@ bool java_bytecode_languaget::typecheck(
     }
   }
 
+  // Add array type clone specializations for enumerations
+  add_java_enum_arrays(symbol_table);
+
   // Now that all classes have been created in the symbol table we can populate
   // the class hierarchy:
   class_hierarchy(symbol_table);