Update parameter documentation

Doxygen produces warnings if some parameters are documentated and not
others, or if there is documentation for parameters which don't exist.

Author: John Nonweiler

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -638,10 +638,8 @@ bool java_entry_point(
 /// \param message_handler: Where to write output to
 /// \param assume_init_pointers_not_null: When creating pointers, assume they
 ///   always take a non-null value.
-/// \param max_nondet_array_length: The length of the arrays to create when
-///   filling them
-/// \param max_nondet_tree_depth: defines the maximum depth of the object tree
-///   (see java_entry_points documentation for details)
+/// \param assert_uncaught_exceptions: Add an uncaught-exception check
+/// \param object_factory_parameters: Parameters for creation of arguments
 /// \param pointer_type_selector: Logic for substituting types of pointers
 /// \returns true if error occurred on entry point search, false otherwise
 bool generate_java_start_function(

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -176,6 +176,7 @@ class java_object_factoryt
 /// \param allocate_type: type of the object allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
+/// \param function_id: function ID to associate with auxiliary variables
 /// \param output_code: code block to which the necessary code is added
 /// \param symbols_created: created symbols to be declared by the caller
 /// \param cast_needed: Boolean flags saying where we need to cast the malloc
@@ -242,6 +243,7 @@ exprt allocate_dynamic_object(
 ///   allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
+/// \param function_id: function ID to associate with auxiliary variables
 /// \param output_code: code block to which the necessary code is added
 /// \return the dynamic object created
 exprt allocate_dynamic_object_with_decl(
@@ -392,6 +394,8 @@ code_assignt java_object_factoryt::get_null_assignment(
 ///   NO_UPDATE_IN_PLACE: initialize `expr` from scratch
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
 ///   MAY_UPDATE_IN_PLACE: invalid input
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_pointer_target_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -707,6 +711,8 @@ bool initialize_nondet_string_fields(
 ///   * MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
 ///     and MUST_ cases.
 ///   * MUST_UPDATE_IN_PLACE: reinitialize an existing object
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_pointer_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -930,6 +936,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
+/// \param location:
+///   Source location associated with nondet-initialization.
 /// \return
 ///   A symbol expression of type \p replacement_pointer corresponding to a
 ///   pointer to object `tmp_object` (see above).
@@ -994,6 +1002,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
 ///   NO_UPDATE_IN_PLACE: initialize `expr` from scratch
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
 ///   MAY_UPDATE_IN_PLACE: invalid input
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_struct_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -1159,6 +1169,8 @@ void java_object_factoryt::gen_nondet_struct_init(
 ///   MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
 ///   and MUST_ cases.
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -1307,6 +1319,8 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
 /// \param element_type:
 ///   Actual element type of the array (the array for all reference types will
 ///   have void* type, but this will be annotated as the true member type).
+/// \param location:
+///   Source location associated with nondet-initialization.
 /// \return Appends instructions to `assignments`
 void java_object_factoryt::allocate_nondet_length_array(
   code_blockt &assignments,

jbmc/src/java_bytecode/java_types.h

@@ -695,8 +695,8 @@ inline typet java_type_from_string_with_exception(
 }
 
 /// Get the index in the subtypes array for a given component.
-/// \param t The type we search for the subtypes in.
-/// \param identifier The string identifier of the type of the component.
+/// \param gen_types: The subtypes array.
+/// \param identifier: The string identifier of the type of the component.
 /// \return Optional with the size if the identifier was found.
 inline const optionalt<size_t> java_generics_get_index_for_subtype(
   const std::vector<java_generic_parametert> &gen_types,

src/goto-programs/class_hierarchy.h

@@ -130,7 +130,6 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
 /// Output the class hierarchy
 /// \param hierarchy: the class hierarchy to be printed
 /// \param message_handler: the message handler
-/// \param ui: the UI format
 /// \param children_only: print the children only and do not print the parents
 void show_class_hierarchy(
   const class_hierarchyt &hierarchy,

src/goto-programs/read_goto_binary.cpp

@@ -260,8 +260,10 @@ bool read_object_and_link(
 }
 
 /// \brief reads an object file, and also updates the config
-/// \param file_name file name of the goto binary
-/// \param message_handler for diagnostics
+/// \param file_name: file name of the goto binary
+/// \param dest_symbol_table: symbol table to update
+/// \param dest_functions: collection of goto functions to update
+/// \param message_handler: for diagnostics
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,