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 00000000000..b88e1234be9 Binary files /dev/null and b/jbmc/regression/jbmc/main-method-ambiguity/Test.class differ 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 {