Skip to content

Commit bbe8cca

Browse files
Java main method must be public
1 parent 86687f7 commit bbe8cca

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

jbmc/src/java_bytecode/java_entry_point.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -274,12 +274,14 @@ exprt::operandst java_build_arguments(
274274
bool named_main=has_suffix(config.main, ".main");
275275
const typet &string_array_type=
276276
java_type_from_string("[Ljava.lang.String;");
277+
// checks whether the function is static and has a single String[] parameter
277278
bool has_correct_type=
278279
to_code_type(function.type).return_type().id()==ID_empty &&
279280
(!to_code_type(function.type).has_this()) &&
280281
parameters.size()==1 &&
281282
parameters[0].type().full_eq(string_array_type);
282-
is_main=(named_main && has_correct_type);
283+
bool public_access = function.type.get(ID_access) == ID_public;
284+
is_main = named_main && has_correct_type && public_access;
283285
}
284286

285287
// we iterate through all the parameters of the function under test, allocate

0 commit comments

Comments
 (0)