Java entry point / main function

Restructure finding of the entry point of the Java function or the main function
of the program.

Author: Matthias Güdemann

src/java_bytecode/java_bytecode_language.cpp

@@ -6,6 +6,8 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <string>
+
 #include <util/symbol_table.h>
 #include <util/suffix.h>
 #include <util/config.h>
@@ -39,9 +41,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet& cmd)
   disable_runtime_checks=cmd.isset("disable-runtime-check");
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   if(cmd.isset("java-max-input-array-length"))
-    max_nondet_array_length=safe_string2int(cmd.get_value("java-max-input-array-length"));
+    max_nondet_array_length=std::stoi(cmd.get_value("java-max-input-array-length"));
   if(cmd.isset("java-max-vla-length"))
-    max_user_array_length=safe_string2int(cmd.get_value("java-max-vla-length"));
+    max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
 }
 
 /*******************************************************************\
@@ -229,11 +231,12 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   java_internal_additions(symbol_table);
 
 
-  std::tuple<symbolt, bool, bool> t = get_main_symbol(symbol_table, main_class, get_message_handler());
-  if(std::get<2>(t))
-    return std::get<1>(t);
+  main_function_resultt res=
+    get_main_symbol(symbol_table, main_class, get_message_handler());
+  if(res.stop_convert)
+    return res.error_found;
 
-  symbolt entry = std::get<0>(t);
+  symbolt entry=res.main_function;
 
   if(java_entry_point(symbol_table,main_class,get_message_handler(),
 		      assume_inputs_non_null,max_nondet_array_length))

src/java_bytecode/java_bytecode_language.h

@@ -69,10 +69,15 @@ class java_bytecode_languaget:public languaget
 protected:
   irep_idt main_class;
   java_class_loadert java_class_loader;
-  bool assume_inputs_non_null;
-  bool disable_runtime_checks;
-  int max_nondet_array_length;
-  int max_user_array_length;
+  bool assume_inputs_non_null;      // assume inputs variables to be non-null
+
+  bool disable_runtime_checks;      // disable run-time checks for java, i.e.,
+                                    // ASSERTS for
+                                    //  - checkcast / instanceof
+                                    //  - array bounds check
+                                    //  - array size for newarray
+  size_t max_nondet_array_length;   // maximal length for non-det array creation
+  size_t max_user_array_length;     // max size for user supplied arrays
 };
 
 languaget *new_java_bytecode_language();