the main_class is now remembered in the symbol table

Author: Daniel Kroening

src/java_bytecode/ci_lazy_methods.cpp

@@ -61,7 +61,8 @@ bool ci_lazy_methodst::operator()(
   std::vector<irep_idt> method_worklist2;
 
   auto main_function=
-    get_main_symbol(symbol_table, main_class, get_message_handler(), true);
+    get_main_symbol(symbol_table, get_message_handler(), true);
+
   if(main_function.stop_convert)
   {
     // Failed, mark all functions in the given main class(es)

src/java_bytecode/java_bytecode_language.cpp

@@ -236,6 +236,18 @@ bool java_bytecode_languaget::typecheck(
        symbol_table, get_message_handler(), string_refinement_enabled))
     return true;
 
+  // remember the main class, if any
+  if(!main_class.empty())
+  {
+    symbolt main_class_symbol;
+    main_class_symbol.name="java_main_class";
+    main_class_symbol.base_name=main_class_symbol.name;
+    main_class_symbol.value.id(ID_string_constant);
+    main_class_symbol.value.set(ID_value, main_class);
+    main_class_symbol.mode=ID_java;
+    symbol_table.move(main_class_symbol);
+  }
+
   return false;
 }
 
@@ -368,15 +380,14 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   replace_string_methods(symbol_table);
 
   main_function_resultt res=
-    get_main_symbol(symbol_table, main_class, get_message_handler());
+    get_main_symbol(symbol_table, get_message_handler());
   if(res.stop_convert)
     return res.error_found;
 
   // generate the test harness in __CPROVER__start and a call the entry point
   return
     java_entry_point(
       symbol_table,
-      main_class,
       get_message_handler(),
       assume_inputs_non_null,
       max_nondet_array_length,

src/java_bytecode/java_entry_point.cpp

@@ -322,7 +322,6 @@ void java_record_outputs(
 
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &message_handler,
   bool allow_no_body)
 {
@@ -362,7 +361,7 @@ main_function_resultt get_main_symbol(
     // check if it has a body
     if(symbol.value.is_nil() && !allow_no_body)
     {
-      message.error() << "main method `" << main_class
+      message.error() << "main method `" << symbol.display_name()
                       << "' has no body" << messaget::eom;
       res.main_function=symbol;
       res.error_found=true;
@@ -375,15 +374,20 @@ main_function_resultt get_main_symbol(
     // no function given, we look for the main class
     assert(config.main=="");
 
+    symbol_tablet::symbolst::const_iterator s_it=
+      symbol_table.symbols.find("java_main_class");
+
     // are we given a main class?
-    if(main_class.empty())
+    if(s_it==symbol_table.symbols.end())
     {
       res.main_function=symbol;
       res.error_found=false;
       res.stop_convert=true;
       return res; // silently ignore
     }
 
+    irep_idt main_class=s_it->second.value.get(ID_value);
+
     std::string entry_method=
       id2string(main_class)+".main";
 
@@ -478,7 +482,6 @@ main_function_resultt get_main_symbol(
 /// \returns true if error occurred on entry point search
 bool java_entry_point(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   size_t max_nondet_array_length,
@@ -492,7 +495,7 @@ bool java_entry_point(
 
   messaget message(message_handler);
   main_function_resultt res=
-    get_main_symbol(symbol_table, main_class, message_handler);
+    get_main_symbol(symbol_table, message_handler);
   if(res.stop_convert)
     return res.stop_convert;
   symbolt symbol=res.main_function;

src/java_bytecode/java_entry_point.h

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 
 bool java_entry_point(
   class symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   size_t max_nondet_array_length,
@@ -36,7 +35,6 @@ typedef struct
 /// Figures out the entry point of the code to verify
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &,
   bool allow_no_body=false);