Merge pull request #7139 from tautschnig/fixes/doxygen

Fix Doxygen comment issues

Author: tautschnig

jbmc/src/java_bytecode/README.md

@@ -659,7 +659,7 @@ when they are in some way requested.
 
 The mechanism used to achieve this is initially common to both eager and
 context-insensitive lazy loading. \ref java_bytecode_languaget::typecheck calls
-[java_bytecode_convert_class](\ref java_bytecode_languaget::java_bytecode_convert_class)
+[java_bytecode_convert_class](\ref java_bytecode_convert_class)
 (for each class loaded by the class loader) to create symbols for all classes
 and the methods in them. The methods, along with their parsed representation
 (including bytecode) are also added to a map called
@@ -672,7 +672,7 @@ determine which loading strategy to use.
 \subsection eager-loading Eager loading
 
 If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
-\ref java_bytecode_languaget::LAZY_METHODS_MODE_EAGER then eager loading is
+\ref LAZY_METHODS_MODE_EAGER then eager loading is
 used. Under eager loading
 \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &)
 is called once for each method listed in method_bytecode (described above). This
@@ -696,7 +696,7 @@ locate further classes and methods to load. The following paragraph describes
 the mechanism used.
 
 If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
-\ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then
+\ref LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then
 context-insensitive lazy loading is used. Under this stragegy
 \ref java_bytecode_languaget::do_ci_lazy_method_conversion is called to do all
 conversion. This calls `operator()` of \ref ci_lazy_methodst,

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -120,7 +120,7 @@ class java_bytecode_convert_classt
   ///
   /// An overlay method is a method with the annotation
   /// \@OverlayMethodImplementation. They should only appear in
-  /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class). They
+  /// [overlay classes](\ref is_overlay_class). They
   /// will be loaded by JBMC instead of the method with the same signature
   /// in the underlying class. It is an error if there is no method with the
   /// same signature in the underlying class. It is an error if a method in
@@ -142,7 +142,7 @@ class java_bytecode_convert_classt
   ///
   /// 2. If it has the annotation\@IgnoredMethodImplementation.
   /// This kind of ignord method is intended for use in
-  /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class), in
+  /// [overlay classes](\ref is_overlay_class), in
   /// particular for methods which must exist in the overlay class so that
   /// it will compile, e.g. default constructors, but which we do not want
   /// to overlay the corresponding method in the

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -48,15 +48,15 @@ Author: Daniel Kroening, [email protected]
 /// Iterates through the parameters of the function type \p ftype, finds a new
 /// new name for each parameter and renames them in `ftype.parameters()` as
 /// well as in the \p symbol_table.
+/// Assigns parameter names (side-effects on `ftype`) to function stub
+/// parameters, which are initially nameless as method conversion hasn't
+/// happened. Also creates symbols in `symbol_table`.
 /// \param [in,out] ftype:
 ///   Function type whose parameters should be named.
 /// \param name_prefix:
 ///   Prefix for parameter names, typically the parent function's name.
 /// \param [in,out] symbol_table:
 ///   Global symbol table.
-/// \return Assigns parameter names (side-effects on `ftype`) to function stub
-///   parameters, which are initially nameless as method conversion hasn't
-///   happened. Also creates symbols in `symbol_table`.
 static void assign_parameter_names(
   java_method_typet &ftype,
   const irep_idt &name_prefix,

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1156,9 +1156,9 @@ const select_pointer_typet &
 
 /// Provide feedback to `language_filest` so that when asked for a lazy method,
 /// it can delegate to this instance of java_bytecode_languaget.
-/// \return Populates `methods` with the complete list of lazy methods that are
-///   available to convert (those which are valid parameters for
-///   `convert_lazy_method`)
+/// \param [out] methods: Populates `methods` with the complete list of lazy
+///   methods that are available to convert (those which are valid parameters
+///   for `convert_lazy_method`)
 void java_bytecode_languaget::methods_provided(
   std::unordered_set<irep_idt> &methods) const
 {

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1138,7 +1138,6 @@ void java_object_factoryt::declare_created_symbols(code_blockt &init_code)
 ///   A function to generate a new local symbol and add it to the symbol table
 /// \param location:
 ///   Source location associated with nondet-initialization.
-/// \return Appends instructions to `assignments`
 static void allocate_nondet_length_array(
   code_blockt &assignments,
   const exprt &lhs,

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -23,7 +23,7 @@ Author: Chris Smowton, [email protected]
 #include <sstream>
 
 /// Convert UCS-2 or UTF-16 to an array expression.
-/// \par parameters: `in`: wide string to convert
+/// \param in: wide string to convert
 /// \return Returns a Java char array containing the same wchars.
 static array_exprt utf16_to_array(const std::wstring &in)
 {

jbmc/src/java_bytecode/nondet.h

@@ -22,9 +22,8 @@ using allocate_local_symbolt =
 ///   const mp_integer &max_value,
 ///   const std::string &name_prefix,
 ///   const typet &int_type,
-///   const irep_idt &mode,
 ///   const source_locationt &source_location,
-///   symbol_table_baset &symbol_table,
+///   allocate_objectst &allocate_objects,
 ///   code_blockt &instructions)
 /// except the minimum and maximum values are represented as exprts.
 symbol_exprt generate_nondet_int(
@@ -35,6 +34,16 @@ symbol_exprt generate_nondet_int(
   allocate_objectst &allocate_objects,
   code_blockt &instructions);
 
+/// Same as \ref generate_nondet_int(
+///   const mp_integer &min_value,
+///   const mp_integer &max_value,
+///   const std::string &name_prefix,
+///   const typet &int_type,
+///   const source_locationt &source_location,
+///   allocate_objectst &allocate_objects,
+///   code_blockt &instructions)
+/// except the minimum and maximum values are represented as exprts, and symbols
+/// are allocated using \ref allocate_local_symbolt.
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
   const exprt &max_value_expr,

src/analyses/README.md

@@ -95,7 +95,7 @@ To be documented.
 
 Implemented in `src/analyses/dependence_graph.h(cpp)`. It is a graph and an
 abstract interpreter at the same time. The abstract interpretation nature
-allows a dependence graph to [build itself](#Construction)
+allows a dependence graph to [build itself](Construction)
 (the graph) from a given GOTO program.
 
 A dependence graph extends the class `grapht` with `dep_nodet` as the type of

src/analyses/cfg_dominators.h

@@ -256,7 +256,8 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
 
 /// Pretty-print a single node in the dominator tree. Supply a specialisation if
 /// operator<< is not sufficient.
-/// \par parameters: `node` to print and stream `out` to pretty-print it to
+/// \param node: node to print
+/// \param out: stream to pretty-print it to
 template <class T>
 void dominators_pretty_print_node(const T &node, std::ostream &out)
 {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -93,7 +93,7 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
 protected:
   CLONE
 
-  /// \copydoc abstract_object::merge
+  /// \copydoc abstract_objectt::merge
   abstract_object_pointert merge(
     const abstract_object_pointert &other,
     const widen_modet &widen_mode) const override;

src/cpp/cpp_scopes.cpp

@@ -69,7 +69,6 @@ cpp_idt &cpp_scopest::put_into_scope(
   }
 }
 
-/// \return Purpose:
 void cpp_scopest::print_current(std::ostream &out) const
 {
   const cpp_scopet *scope=current_scope_ptr;

src/goto-cc/goto_cc_mode.cpp

@@ -131,8 +131,7 @@ int goto_cc_modet::main(int argc, const char **argv)
   }
 }
 
-/// prints a message informing the user about incorrect options
-/// \return none
+/// Prints a message informing the user about incorrect options.
 void goto_cc_modet::usage_error()
 {
   std::cerr << "Usage error!\n\n";

src/goto-cc/ms_cl_cmdline.cpp

@@ -97,7 +97,6 @@ bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
   return false;
 }
 
-/// \return none
 void ms_cl_cmdlinet::parse_env()
 {
   // first do environment
@@ -170,7 +169,6 @@ static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
   return in;
 }
 
-/// \return none
 void ms_cl_cmdlinet::process_response_file(const std::string &file)
 {
   std::ifstream infile(file);
@@ -231,7 +229,6 @@ void ms_cl_cmdlinet::process_response_file(const std::string &file)
   }
 }
 
-/// \return none
 void ms_cl_cmdlinet::process_response_file_line(const std::string &line)
 {
   // In a response file, multiple compiler options and source-code files can
@@ -271,7 +268,6 @@ void ms_cl_cmdlinet::process_response_file_line(const std::string &line)
   parse(arguments);
 }
 
-/// \return none
 void ms_cl_cmdlinet::process_non_cl_option(
   const std::string &s)
 {

src/goto-cc/ms_link_cmdline.cpp

@@ -106,7 +106,6 @@ static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
   return in;
 }
 
-/// \return none
 void ms_link_cmdlinet::process_response_file(const std::string &file)
 {
   std::ifstream infile(file);
@@ -166,7 +165,6 @@ void ms_link_cmdlinet::process_response_file(const std::string &file)
   }
 }
 
-/// \return none
 void ms_link_cmdlinet::process_response_file_line(const std::string &line)
 {
   // In a response file, multiple compiler options and source-code files can
@@ -206,7 +204,6 @@ void ms_link_cmdlinet::process_response_file_line(const std::string &line)
   parse(arguments);
 }
 
-/// \return none
 void ms_link_cmdlinet::process_non_link_option(const std::string &s)
 {
   set(s);

src/goto-programs/README.md

@@ -631,7 +631,7 @@ returned from.
 
 If the function has a return value, an \ref assignment-step-structure
 assignment will be made to a variable with identifier with suffix
-\ref remove_returns::RETURN_VALUE_SUFFIX.
+\ref RETURN_VALUE_SUFFIX.
 
 \subsection assignment-step-structure Assignment
 

src/solvers/strings/string_refinement.cpp

@@ -291,13 +291,12 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 }
 
 /// Add association for each char pointer in the equation
-/// \param symbol_solver: a union_find_replacet object to keep track of
-///   char pointer equations
+/// \param [in,out] symbol_solver: a union_find_replacet object to keep track of
+///   char pointer equations. Char pointers that have been set equal by an
+///   equation are associated to the same element.
 /// \param equations: vector of equations
 /// \param ns: namespace
 /// \param stream: output stream
-/// \return union_find_replacet where char pointer that have been set equal
-///   by an equation are associated to the same element
 static void add_equations_for_symbol_resolution(
   union_find_replacet &symbol_solver,
   const std::vector<exprt> &equations,