Java frontend: clean up unused clinit symbols

Previously clinit wrappers that had been generated but never actually called would
remain in the GOTO program as empty, uncalled functions. Now they are cleaned up
in the same way as unused user functions.

Author: smowton

src/java_bytecode/ci_lazy_methods.cpp

@@ -36,14 +36,16 @@ ci_lazy_methodst::ci_lazy_methodst(
   java_class_loadert &java_class_loader,
   const std::vector<irep_idt> &extra_needed_classes,
   const select_pointer_typet &pointer_type_selector,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const synthetic_methods_mapt &synthetic_methods)
   : messaget(message_handler),
     main_class(main_class),
     main_jar_classes(main_jar_classes),
     lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),
     java_class_loader(java_class_loader),
     extra_needed_classes(extra_needed_classes),
-    pointer_type_selector(pointer_type_selector)
+    pointer_type_selector(pointer_type_selector),
+    synthetic_methods(synthetic_methods)
 {
   // build the class hierarchy
   class_hierarchy(symbol_table);
@@ -196,7 +198,8 @@ bool ci_lazy_methodst::operator()(
       // Don't keep functions that belong to this language that we haven't
       // converted above
       if(
-        method_bytecode.contains_method(sym.first) &&
+        (method_bytecode.contains_method(sym.first) ||
+         synthetic_methods.count(sym.first)) &&
         !methods_already_populated.count(sym.first))
       {
         continue;

src/java_bytecode/ci_lazy_methods.h

@@ -23,6 +23,7 @@
 #include <java_bytecode/java_class_loader.h>
 #include <java_bytecode/ci_lazy_methods_needed.h>
 #include <java_bytecode/select_pointer_type.h>
+#include <java_bytecode/synthetic_methods_map.h>
 
 class java_string_library_preprocesst;
 
@@ -99,7 +100,8 @@ class ci_lazy_methodst:public messaget
     java_class_loadert &java_class_loader,
     const std::vector<irep_idt> &extra_needed_classes,
     const select_pointer_typet &pointer_type_selector,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    const synthetic_methods_mapt &synthetic_methods);
 
   // not const since messaget
   bool operator()(
@@ -164,6 +166,7 @@ class ci_lazy_methodst:public messaget
   java_class_loadert &java_class_loader;
   const std::vector<irep_idt> &extra_needed_classes;
   const select_pointer_typet &pointer_type_selector;
+  const synthetic_methods_mapt &synthetic_methods;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H

src/java_bytecode/java_bytecode_language.cpp

@@ -688,7 +688,8 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
     java_class_loader,
     java_load_classes,
     get_pointer_type_selector(),
-    get_message_handler());
+    get_message_handler(),
+    synthetic_methods);
 
   return method_gather(symbol_table, method_bytecode, method_converter);
 }