Improve documentation of convert_java_nondet

In particular highlight the need to run remove_java_new *after* this pass.

Author: smowton

jbmc/src/java_bytecode/convert_java_nondet.h

@@ -7,7 +7,7 @@ Author: Reuben Thomas, [email protected]
 \*******************************************************************/
 
 /// \file
-/// Convert side_effect_expr_nondett expressions
+/// Convert side_effect_expr_nondett expressions using java_object_factory
 
 #ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 #define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
@@ -22,8 +22,15 @@ class goto_model_functiont;
 class message_handlert;
 struct object_factory_parameterst;
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation.
+/// Converts side_effect_exprt_nondett expressions using java_object_factory.
+/// For example, NONDET(SomeClass *) may become a nondet choice between a null
+/// pointer and a fresh instance of SomeClass, whose fields are in turn nondet
+/// initialized in the same way. See \ref java_object_factory.h for details.
+///
+/// Note the code introduced has been freshly `goto_convert`'d without any
+/// passes such as \ref remove_java_new being run. Therefore the caller may need
+/// to (re-)run this and other expected GOTO transformations after this pass
+/// completes.
 /// \param goto_functions: The set of goto programs to modify.
 /// \param symbol_table: The symbol table to query/update.
 /// \param message_handler: For error logging.
@@ -40,8 +47,15 @@ void convert_nondet(
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation.
+/// Converts side_effect_exprt_nondett expressions using java_object_factory.
+/// For example, NONDET(SomeClass *) may become a nondet choice between a null
+/// pointer and a fresh instance of SomeClass, whose fields are in turn nondet
+/// initialized in the same way. See \ref java_object_factory.h for details.
+///
+/// Note the code introduced has been freshly `goto_convert`'d without any
+/// passes such as \ref remove_java_new being run. Therefore the caller may need
+/// to (re-)run this and other expected GOTO transformations after this pass
+/// completes.
 /// \param function: goto program to modify
 /// \param message_handler: For error logging.
 /// \param object_factory_parameters: Parameters for the generation of nondet