Implemented generate_start_function for Java

As with the ANSI C version, the Java version undergoes a simmilar
refactor: splitting out the start generation from final so that it can
be regenerated on demand. 2

The entry function in Java now has some parameters that need to passed
to it. Since they are member variables in the java_bytecode_langauge
they can just be passed in from the virtual regenerate call.

Author: thk123

src/java_bytecode/java_bytecode_language.cpp

@@ -106,6 +106,26 @@ void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
   // modules.insert(translation_unit(parse_path));
 }
 
+/// Generate a _start function for a specific function.
+/// \param entry_function_symbol: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool java_bytecode_languaget::generate_start_function(
+  const symbolt &entry_function_symbol,
+  symbol_tablet &symbol_table)
+{
+  return generate_java_start_function(
+    entry_function_symbol,
+    symbol_table,
+    get_message_handler(),
+    assume_inputs_non_null,
+    max_nondet_array_length,
+    max_nondet_tree_depth,
+    *pointer_type_selector);
+}
+
 /// ANSI-C preprocessing
 bool java_bytecode_languaget::preprocess(
   std::istream &instream,

src/java_bytecode/java_bytecode_language.h

@@ -137,6 +137,10 @@ class java_bytecode_languaget:public languaget
   virtual void convert_lazy_method(
     const irep_idt &id, symbol_tablet &) override;
 
+  virtual bool generate_start_function(
+    const class symbolt &entry_function_symbol,
+    class symbol_tablet &symbol_table) override;
+
 protected:
   bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &);
   const select_pointer_typet &get_pointer_type_selector() const;

src/java_bytecode/java_entry_point.cpp

@@ -510,6 +510,32 @@ bool java_entry_point(
     max_nondet_tree_depth,
     pointer_type_selector);
 
+  return generate_java_start_function(
+    symbol,
+    symbol_table,
+    message_handler,
+    assume_init_pointers_not_null,
+    max_nondet_array_length,
+    max_nondet_tree_depth,
+    pointer_type_selector);
+}
+
+/// Generate a _start function for a specific function
+/// \param entry_function_symbol: The symbol for the function that should be
+///   used as the entry point
+/// \param symbol_table: The symbol table for the program. The new _start
+///   function symbol will be added to this table
+/// \return Returns false if the _start method was generated correctly
+bool generate_java_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  size_t max_nondet_array_length,
+  size_t max_nondet_tree_depth,
+  const select_pointer_typet &pointer_type_selector)
+{
+  messaget message(message_handler);
   code_blockt init_code;
 
   // build call to initialization function

src/java_bytecode/java_entry_point.h

@@ -40,4 +40,13 @@ main_function_resultt get_main_symbol(
   message_handlert &,
   bool allow_no_body=false);
 
+bool generate_java_start_function(
+  const symbolt &symbol,
+  class symbol_tablet &symbol_table,
+  class message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  size_t max_nondet_array_length,
+  size_t max_nondet_tree_depth,
+  const select_pointer_typet &pointer_type_selector);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H