Java bytecode front-end: fix main method detection

jbmc/regression/jbmc/main-method-ambiguity/Test.java

@@ -0,0 +1,20 @@
+// Test case for GitHub issue #759
+// CBMC should not produce CONVERSION ERROR when there are multiple
+// methods named 'main' with different signatures.
+// Only the method with signature void main(String[]) is a valid entry point.
+
+public class Test {
+
+    // Invalid main method - no parameters
+    public static void main() {
+    }
+
+    // Valid main method - String[] parameter
+    public static void main(String[] args) {
+        assert false; // This should be the entry point
+    }
+
+    // Invalid main method - single String parameter
+    public static void main(String arg) {
+    }
+}

jbmc/regression/jbmc/main-method-ambiguity/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=(0|10)$
+^SIGNAL=0$
+--
+^CONVERSION ERROR
+^warning: ignoring

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -555,23 +555,52 @@ main_function_resultt get_main_symbol(
   // find main symbol
   if(config.main.has_value())
   {
-    std::string error_message;
-    irep_idt main_symbol_id = resolve_friendly_method_name(
-      config.main.value(), symbol_table, error_message);
+    std::string config_main = config.main.value();
 
-    if(main_symbol_id.empty())
+    // Check if config.main contains a method signature (has a colon)
+    // If it's just a class name, treat it the same as the main_class parameter
+    if(config_main.find(':') == std::string::npos)
     {
-      message.error()
-        << "main symbol resolution failed: " << error_message << messaget::eom;
-      return main_function_resultt::Error;
+      // config.main is just a class name, remove .class suffix if present
+      if(has_suffix(config_main, ".class"))
+        config_main = config_main.substr(0, config_main.length() - 6);
+
+      // Look for the standard main method
+      std::string entry_method =
+        "java::" + config_main + "." + JAVA_MAIN_METHOD;
+      const symbolt *symbol = symbol_table.lookup(entry_method);
+
+      // has the class a correct main method?
+      if(!symbol || !is_java_main(*symbol))
+      {
+        // no, but we allow this situation to output symbol table,
+        // goto functions, etc
+        return main_function_resultt::NotFound;
+      }
+
+      return *symbol;
     }
+    else
+    {
+      // config.main contains a full method specification, use friendly name resolution
+      std::string error_message;
+      irep_idt main_symbol_id =
+        resolve_friendly_method_name(config_main, symbol_table, error_message);
 
-    const symbolt *symbol = symbol_table.lookup(main_symbol_id);
-    INVARIANT(
-      symbol != nullptr,
-      "resolve_friendly_method_name should return a symbol-table identifier");
+      if(main_symbol_id.empty())
+      {
+        message.error() << "main symbol resolution failed: " << error_message
+                        << messaget::eom;
+        return main_function_resultt::Error;
+      }
 
-    return *symbol; // Return found function
+      const symbolt *symbol = symbol_table.lookup(main_symbol_id);
+      INVARIANT(
+        symbol != nullptr,
+        "resolve_friendly_method_name should return a symbol-table identifier");
+
+      return *symbol; // Return found function
+    }
   }
   else
   {