Merge pull request #3170 from johnnonweiler/doc/reduce-doxygen-warnings-5

Reduce Doxygen warnings

Author: tautschnig

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,

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -323,6 +323,9 @@ static void replace_java_nondet(goto_programt &goto_program)
   }
 }
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation in a single function.
+/// \param function: The goto program to modify.
 void replace_java_nondet(goto_model_functiont &function)
 {
   goto_programt &program = function.get_goto_function().body;
@@ -341,6 +344,9 @@ void replace_java_nondet(goto_functionst &goto_functions)
   remove_skip(goto_functions);
 }
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation.
+/// \param goto_model: The goto program to modify.
 void replace_java_nondet(goto_modelt &goto_model)
 {
   replace_java_nondet(goto_model.goto_functions);

jbmc/src/java_bytecode/replace_java_nondet.h

@@ -16,16 +16,10 @@ class goto_modelt;
 class goto_functionst;
 class goto_model_functiont;
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation.
-/// \param goto_model: The goto program to modify.
 void replace_java_nondet(goto_modelt &);
 
 void replace_java_nondet(goto_functionst &);
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation in a single function.
-/// \param function: The goto program to modify.
 void replace_java_nondet(goto_model_functiont &function);
 
 #endif

src/cbmc/xml_interface.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/cmdline.h>
 
+class xmlt;
+
 class xml_interfacet
 {
 public:
@@ -24,7 +26,7 @@ class xml_interfacet
 
 protected:
   void get_xml_options(cmdlinet &cmdline);
-  void get_xml_options(const class xmlt &xml, cmdlinet &cmdline);
+  void get_xml_options(const xmlt &xml, cmdlinet &cmdline);
 };
 
 #endif // CPROVER_CBMC_XML_INTERFACE_H

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,

src/util/options.cpp

@@ -27,14 +27,12 @@ void optionst::set_option(const std::string &option,
   set_option(option, std::string(value?"1":"0"));
 }
 
-void optionst::set_option(const std::string &option,
-                          const signed int value)
+void optionst::set_option(const std::string &option, const int value)
 {
   set_option(option, std::to_string(value));
 }
 
-void optionst::set_option(const std::string &option,
-                          const unsigned int value)
+void optionst::set_option(const std::string &option, const unsigned value)
 {
   set_option(option, std::to_string(value));
 }