Skip to content

Commit 12ca989

Browse files
Document class_identifier argument of root class
This can prevent mistake in forgetting the "java::" prefix.
1 parent 5524078 commit 12ca989

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/java_bytecode/java_root_class.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,8 @@ void java_root_class(symbolt &class_symbol)
5757
/// \param jlo [out] : object to initialize
5858
/// \param root_type: type of the root class
5959
/// \param lock: lock field
60-
/// \param class_identifier: class identifier field
60+
/// \param class_identifier: class identifier field, generally begins with
61+
/// "java::" prefix.
6162
void java_root_class_init(
6263
struct_exprt &jlo,
6364
const struct_typet &root_type,

0 commit comments

Comments
 (0)