Update parameter documentation in Doxygen comments

Author: John Nonweiler

scripts/expected_doxygen_warnings.txt

@@ -76,13 +76,6 @@
 /cbmc/src/ansi-c/expr2c_class.h:54: warning: The following parameters of expr2ct::convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str) are not documented:
   parameter 'qualifiers_str'
   parameter 'declarator_str'
-/cbmc/src/goto-programs/goto_convert_class.h:584: warning: The following parameters of goto_convertt::generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode) are not documented:
-  parameter 'mode'
-/cbmc/src/goto-programs/goto_model.h:150: warning: argument 'goto_model' of command @param is not found in the argument list of goto_model_functiont::goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function)
-/cbmc/src/goto-programs/goto_model.h:155: warning: The following parameters of goto_model_functiont::goto_model_functiont(journalling_symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function) are not documented:
-  parameter 'symbol_table'
-  parameter 'goto_functions'
-  parameter 'function_id'
 /cbmc/src/goto-instrument/wmm/goto2graph.h:260: warning: The following parameters of instrumentert::cfg_visitort::visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, std::set< nodet > &ending_vertex) are not documented:
   parameter 'model'
   parameter 'no_dependencies'
@@ -124,18 +117,12 @@
 /cbmc/src/langapi/language.cpp:121: warning: argument 'parameter_type' of command @param is not found in the argument list of languaget::build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert &parameter)
 /cbmc/src/langapi/language.h:176: warning: The following parameters of languaget::build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert &parameter) are not documented:
   parameter 'parameter'
-/cbmc/src/goto-programs/rebuild_goto_start_function.h:31: warning: The following parameters of rebuild_goto_start_function_baset::rebuild_goto_start_function_baset(const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler) are not documented:
-  parameter 'options'
-  parameter 'message_handler'
-/cbmc/src/goto-programs/rebuild_goto_start_function.cpp:37: warning: argument 'entry_function' of command @param is not found in the argument list of rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(void)
 /cbmc/jbmc/src/java_bytecode/remove_exceptions.cpp:47: warning: Found unknown command `\class_identifier'
 /cbmc/jbmc/src/java_bytecode/select_pointer_type.h:50: warning: The following parameters of select_pointer_typet::specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const are not documented:
   parameter 'visited_nodes'
 /cbmc/src/solvers/refinement/string_refinement.cpp:2099: warning: argument 'expr' of command @param is not found in the argument list of string_constraintt::universal_only_in_index(const string_constraintt &constr)
 /cbmc/src/solvers/refinement/string_refinement.cpp:2106: warning: The following parameters of string_constraintt::universal_only_in_index(const string_constraintt &constr) are not documented:
   parameter 'constr'
-/cbmc/src/goto-programs/goto_trace.cpp:132: warning: The following parameters of numeric_representation(const constant_exprt &expr, const namespacet &ns, const trace_optionst &options) are not documented:
-  parameter 'ns'
 /cbmc/jbmc/src/java_bytecode/README.md:26: warning: unable to resolve reference to `java-bytecode-remove-instance-of' for \ref command
 /cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved
 /cbmc/jbmc/src/java_bytecode/README.md:89: warning: explicit link request to 'define' could not be resolved
@@ -146,4 +133,3 @@
 /cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_new_symbol_table' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns)
 /cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_options' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns)
 /cbmc/src/pointer-analysis/dereference.h:26: warning: argument '_dereference_callback' of command @param is not found in the argument list of dereferencet::dereferencet(const namespacet &_ns)
-/cbmc/src/goto-programs/rebuild_goto_start_function.cpp:22: warning: argument '_message_handler' of command @param is not found in the argument list of rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::rebuild_goto_start_function_baset(const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler)

src/goto-programs/goto_convert.cpp

@@ -1971,9 +1971,10 @@ void goto_convert(
 /// E: END_THREAD
 /// Z: SKIP
 ///
-/// \param thread_body: sequence of codet's that can be executed
-///   in parallel.
-/// \param [out] dest: resulting goto-instructions.
+/// \param thread_body: Sequence of codet's that can be executed
+///   in parallel
+/// \param [out] dest: Resulting goto-instructions
+/// \param mode: Language mode
 void goto_convertt::generate_thread_block(
   const code_blockt &thread_body,
   goto_programt &dest,

src/goto-programs/goto_model.h

@@ -154,10 +154,14 @@ class goto_model_functiont
 {
 public:
   /// Construct a function wrapper
-  /// \param goto_model: will be used to ensure unique numbering of
-  ///   goto programs, specifically incrementing its unused_location_number
-  ///   member each time a program is re-numbered.
-  /// \param goto_function: function to wrap.
+  /// \param symbol_table: Symbol table where any new symbols associated with
+  ///   `goto_function` should be inserted
+  /// \param goto_functions: `goto_functionst` that contains `goto_function`.
+  ///   Only used to ensure unique numbering of `goto_function`, specifically
+  ///   incrementing its `unused_location_number` member each time the program
+  ///   is re-numbered.
+  /// \param function_id: Name of function to wrap
+  /// \param goto_function: Function to wrap
   goto_model_functiont(
     journalling_symbol_tablet &symbol_table,
     goto_functionst &goto_functions,

src/goto-programs/goto_trace.cpp

@@ -127,6 +127,7 @@ void goto_trace_stept::output(
 /// options.base_prefix to be true appends either 0b or 0x to the number
 /// to indicate the base
 /// \param expr: expression to get numeric representation from
+/// \param ns: namespace for symbol type lookups
 /// \param options: configuration options
 /// \return a string with the numeric representation
 static std::string numeric_representation(

src/goto-programs/rebuild_goto_start_function.cpp

@@ -20,10 +20,11 @@
 
 /// To rebuild the _start function in the event the program was compiled into
 /// GOTO with a different entry function selected.
+/// \param options: Command-line options
 /// \param goto_model: The goto functions (to replace the body of the _start
 ///   function) and symbol table (to replace the _start function symbol) of the
 ///   program.
-/// \param _message_handler: The message handler to report any messages with
+/// \param message_handler: The message handler to report any messages with
 template <typename maybe_lazy_goto_modelt>
 rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
   rebuild_goto_start_function_baset(
@@ -38,8 +39,6 @@ rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
 /// GOTO with a different entry function selected. It works by discarding the
 /// _start symbol and GOTO function and calling on the relevant languaget to
 /// generate the _start function again.
-/// \param entry_function: The name of the entry function that should be
-/// called from _start
 /// \return Returns true if either the symbol is not found, or something went
 ///   wrong with generating the start_function. False otherwise.
 template<typename maybe_lazy_goto_modelt>