From 6afa932e9632f8520ef32cd0de36b3606f87de28 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Nov 2025 19:53:11 +0100
Subject: [PATCH] Java bytecode front-end: fix main method detection

When parsing Java classes with just a class name (without method signature),
JBMC was incorrectly using `resolve_friendly_method_name` which could report
'main method is ambiguous' errors. This fix checks if `config.main` contains
a method signature (has a colon) and handles simple class names separately
by looking for the standard main method signature directly.

This aligns the Java front-end with Java's specification, where only
`public static void main(String[] args)` is recognized as a valid
program entry point.

Fixes: #759
---
 .../jbmc/main-method-ambiguity/Test.class     | Bin 0 -> 616 bytes
 .../jbmc/main-method-ambiguity/Test.java      |  20 +++++++
 .../jbmc/main-method-ambiguity/test.desc      |   8 +++
 jbmc/src/java_bytecode/java_entry_point.cpp   |  53 ++++++++++++++----
 4 files changed, 69 insertions(+), 12 deletions(-)
 create mode 100644 jbmc/regression/jbmc/main-method-ambiguity/Test.class
 create mode 100644 jbmc/regression/jbmc/main-method-ambiguity/Test.java
 create mode 100644 jbmc/regression/jbmc/main-method-ambiguity/test.desc

diff --git a/jbmc/regression/jbmc/main-method-ambiguity/Test.class b/jbmc/regression/jbmc/main-method-ambiguity/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..b88e1234be96e2a524edc55b56f7eb11e7216147
GIT binary patch
literal 616
zcmZvZ%TB^T6o&t43x!fBiWl%26Bp=0H|{h><7MS#0Wncm1tw$=ikTK4#usp{CYorX
zdmqYpP6Kp-Z8Dvi^PlfO=k(|I;|stcRvj2HZCEZ+NDCA@{)4~W^@H~IWuqgTkwAJ+
z1uEJXFsmC^S!9s4;kd}b6|m|uBuQ!A4@0RV)epjB75a^?Yzc@P8wG)Kf;=3lPPFc8
z2YHwdrZ8=z<YET10$w6M>Jn67t|ddIWow*Ui~MLn0V?N)Dmd!5B;}o{Kwb=b4XNvF
zPl2AV0!pvmo+Zp$q*c(~-MA9S6Q_B1?%xmfv(^7~nZ0IrH~^>CALyn$Rm{(F>syS*
z8V$vuaf)J@$3nXl1kaP!IXW%VSMcrTJH#^!F;6RpdCj6cmR9J7p9z^0%PN$@#2xbE
zWbXy`BXXa}U%$iqX0{Qt`L_ZEdOa-A&V(q$gvB9&jhHZDRH9~<#`WyPB4BDd^M>Lh
aZ0iY@`3gI+8nwYTDH!enH@i#+11o<d^=G&M

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/main-method-ambiguity/Test.java b/jbmc/regression/jbmc/main-method-ambiguity/Test.java
new file mode 100644
index 00000000000..95097cfd656
--- /dev/null
+++ b/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) {
+    }
+}
diff --git a/jbmc/regression/jbmc/main-method-ambiguity/test.desc b/jbmc/regression/jbmc/main-method-ambiguity/test.desc
new file mode 100644
index 00000000000..89e374c12f3
--- /dev/null
+++ b/jbmc/regression/jbmc/main-method-ambiguity/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=(0|10)$
+^SIGNAL=0$
+--
+^CONVERSION ERROR
+^warning: ignoring
\ No newline at end of file
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index fa074554c8e..a4d1fb8f5f9 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/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
   {