Fix Doxygen comment issues

Doxygen 1.9 detects more inconsistencies that 1.8 did. This commit
addresses all newly reported warnings, which were genuine issues in our
documentation and not artefacts of using version 1.9 instead of 1.8.

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, kroening@kroening.com
 /// 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, chris.smowton@diffblue.com
 #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;