Merge pull request diffblue#3620 from owen-jones-diffblue/fix_doxygen…

…_param_formatting

Fix doxygen param formatting

CODING_STANDARD.md

@@ -70,13 +70,17 @@ Formatting is enforced using clang-format. For more information about this, see
   /// This sentence, until the first dot followed by whitespace, becomes
   /// the brief description. More detailed text follows. Feel free to
   /// break this into paragraphs to aid readability.
-  /// \param arg_name: This parameter doesn't need much description
-  /// \param [out] long_arg_name: This parameter is mutated by the function.
-  ///   Extra info about the parameter gets indented an extra two columns,
+  /// \param arg: This parameter doesn't need much description
+  /// \param long_arg: This parameter needs a long description. Extra
+  ///   information about the parameter gets indented an extra two columns,
   ///   like this.
+  /// \param [out] out_arg: This parameter is mutated by the function, and
+  ///   its value at the beginning of the function is not used
+  /// \param [in,out] in_out_arg: This parameter is mutated by the function, and
+  ///   its value at the beginning of the function is used
   /// \return The return value is literally the value returned by the
-  ///   function. For out-parameters, use "\param [out]".
-  return_typet my_function(argt arg_name, argt &long_arg_name)
+  ///   function. For out-parameters, use "\param [out]" or  "\param [in,out]".
+  ret_typet function(argt arg, argt long_arg, argt &out_arg, argt &in_out_arg)
   ```
 - The priority of documentation is readability. Therefore, feel free to use
   Doxygen features, or to add whitespace for multi-paragraph comment blocks if

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -125,14 +125,13 @@ codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
   return code_assignt(result, expr);
 }
 
-
 /// Converts function call to an assignment of an expression corresponding to
 /// the java method Character.digit:(CI)I. The function call has one character
 /// argument and an optional integer radix argument. If the radix is not given
 /// it is set to 36 by default.
 /// \param target: a position in a goto program
 /// \return code assigning the result of the Character.digit function to the
-///         left-hand-side of the given target
+///   left-hand-side of the given target
 codet character_refine_preprocesst::convert_digit_char(
   conversion_inputt &target)
 {

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -498,7 +498,7 @@ void ci_lazy_methodst::get_virtual_method_targets(
 /// \param e: expression tree to search
 /// \param symbol_table: global symbol table
 /// \param [out] needed: Populated with global variable symbols referenced from
-/// `e` or its children.
+///   `e` or its children.
 void ci_lazy_methodst::gather_needed_globals(
   const exprt &e,
   const symbol_tablet &symbol_table,

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -4,9 +4,9 @@
 
 #include <iterator>
 
-/// \param type Source type
+/// \param type: Source type
 /// \return The vector of implicitly generic and (explicitly) generic type
-/// parameters of the given type.
+///   parameters of the given type.
 const std::vector<java_generic_parametert>
 get_all_generic_parameters(const typet &type)
 {
@@ -37,8 +37,8 @@ get_all_generic_parameters(const typet &type)
 
 /// Add pairs to the controlled map. Own the keys and pop from their stack
 /// on destruction; otherwise do nothing.
-/// \param parameters generic parameters that are the keys of the pairs to add
-/// \param types a type to add for each parameter
+/// \param parameters: generic parameters that are the keys of the pairs to add
+/// \param types: a type to add for each parameter
 void generic_parameter_specialization_map_keyst::insert_pairs(
   const std::vector<java_generic_parametert> &parameters,
   const std::vector<reference_typet> &types)
@@ -87,9 +87,9 @@ void generic_parameter_specialization_map_keyst::insert_pairs(
 /// Add a pair of a parameter and its types for each generic parameter of the
 /// given generic pointer type to the controlled map. Own the keys and pop
 /// from their stack on destruction; otherwise do nothing.
-/// \param pointer_type pointer type to get the specialized generic types from
-/// \param pointer_subtype_struct struct type to which the generic pointer
-/// points, must be generic if the pointer is generic
+/// \param pointer_type: pointer type to get the specialized generic types from
+/// \param pointer_subtype_struct: struct type to which the generic pointer
+///   points, must be generic if the pointer is generic
 void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
   const pointer_typet &pointer_type,
   const typet &pointer_subtype_struct)
@@ -136,9 +136,10 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
 /// in the form of a symbol rather than a pointer (as opposed to the function
 /// insert_pairs_for_pointer). Own the keys and pop from their stack
 /// on destruction; otherwise do nothing.
-/// \param struct_tag_type symbol type to get the specialized generic types from
-/// \param symbol_struct struct type of the symbol type, must be generic if
-/// the symbol is generic
+/// \param struct_tag_type: symbol type to get the specialized generic types
+///   from
+/// \param symbol_struct: struct type of the symbol type, must be generic if
+///   the symbol is generic
 void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
   const struct_tag_typet &struct_tag_type,
   const typet &symbol_struct)

jbmc/src/java_bytecode/jar_file.h

@@ -24,13 +24,13 @@ class jar_filet final
 {
 public:
   /// Open java file for reading.
-  /// \param filename Name of the file
+  /// \param filename: Name of the file
   /// \throw Throws std::runtime_error if file cannot be opened
   explicit jar_filet(const std::string &filename);
 
   /// Open a JAR file of size \p size loaded in memory at address \p data.
-  /// \param data memory buffer with the contents of the jar file
-  /// \param size size  of the memory buffer
+  /// \param data: memory buffer with the contents of the jar file
+  /// \param size: size  of the memory buffer
   /// \throw Throws std::runtime_error if file cannot be opened
   jar_filet(const void *data, size_t size);
 
@@ -42,7 +42,7 @@ class jar_filet final
 
   /// Get contents of a file in the jar archive.
   /// Returns nullopt if file doesn't exist.
-  /// \param filename Name of the file in the archive
+  /// \param filename: Name of the file in the archive
   optionalt<std::string> get_entry(const std::string &filename);
 
   /// Get contents of the Manifest file in the jar archive as a key-value map

jbmc/src/java_bytecode/jar_pool.h

@@ -19,16 +19,16 @@ class jar_poolt
 {
 public:
   /// Load jar archive or retrieve from cache if already loaded
-  /// \param jar_path name of the file
+  /// \param jar_path: name of the file
   // Throws an exception if the file does not exist
   jar_filet &operator()(const std::string &jar_path);
 
-  /// Add a jar archive or retrieve from cache if already added
-  /// \param buffer_name name of the original file
-  /// \param pmem memory pointer to the contents of the file
-  /// \param size size of the memory buffer
+  /// Add a jar archive or retrieve from cache if already added.
   /// Note that this mocks the existence of a file which may
-  /// or may not exist since  the actual data bis retrieved from memory.
+  /// or may not exist since the actual data is retrieved from memory.
+  /// \param buffer_name: name of the original file
+  /// \param pmem: memory pointer to the contents of the file
+  /// \param size: size of the memory buffer
   jar_filet &
   add_jar(const std::string &buffer_name, const void *pmem, size_t size);
 

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -62,7 +62,7 @@ static symbolt add_or_get_symbol(
 /// Retrieve the first label identifier. This is used to mark the start of
 /// a thread block.
 /// /param id: unique thread block identifier
-/// /return: fully qualified label identifier
+/// /return fully qualified label identifier
 static const std::string get_first_label_id(const std::string &id)
 {
   return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
@@ -71,7 +71,7 @@ static const std::string get_first_label_id(const std::string &id)
 /// Retrieve the second label identifier. This is used to mark the end of
 /// a thread block.
 /// /param id: unique thread block identifier
-/// /return: fully qualified label identifier
+/// /return fully qualified label identifier
 static const std::string get_second_label_id(const std::string &id)
 {
   return CPROVER_PREFIX "_THREAD_EXIT_" + id;
@@ -80,7 +80,7 @@ static const std::string get_second_label_id(const std::string &id)
 /// Retrieves a thread block identifier from a function call to
 /// CProver.startThread:(I)V or CProver.endThread:(I)V
 /// /param code: function call to CProver.startThread or CProver.endThread
-/// /return: unique thread block identifier
+/// /return unique thread block identifier
 static const std::string get_thread_block_identifier(
   const code_function_callt &f_code)
 {

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -176,9 +176,9 @@ class java_bytecode_convert_classt:public messaget
 /// - class: A<T> extends B<T, Integer> implements C, D<T>
 /// - signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
 /// - returned superclass reference: B<TT;Ljava/lang/Integer;>;
-/// \param signature Signature of the class
+/// \param signature: Signature of the class
 /// \return Reference of the generic superclass, or empty if the superclass
-/// is not generic
+///   is not generic
 static optionalt<std::string>
 extract_generic_superclass_reference(const optionalt<std::string> &signature)
 {
@@ -215,10 +215,10 @@ extract_generic_superclass_reference(const optionalt<std::string> &signature)
 /// - signature: <T:Ljava/lang/Object;>B<TT;Ljava/lang/Integer;>;LC;LD<TT;>;
 /// - returned interface reference for C: LC;
 /// - returned interface reference for D: LD<TT;>;
-/// \param signature Signature of the class
-/// \param interface_name The interface name
+/// \param signature: Signature of the class
+/// \param interface_name: The interface name
 /// \return Reference of the generic interface, or empty if the interface
-/// is not generic
+///   is not generic
 static optionalt<std::string> extract_generic_interface_reference(
   const optionalt<std::string> &signature,
   const std::string &interface_name)
@@ -982,8 +982,8 @@ bool java_bytecode_convert_class(
 /// Example: if \p parameter has identifier `java::Outer$Inner::T` and
 /// there is a replacement parameter with identifier `java::Outer::T`, the
 /// identifier of \p parameter gets set to `java::Outer::T`.
-/// \param parameter
-/// \param replacement_parameters vector of generic parameters (only viable
+/// \param parameter: The given generic type parameter
+/// \param replacement_parameters: vector of generic parameters (only viable
 ///   ones, i.e., only those that can actually appear here such as generic
 ///   parameters of outer classes of the class specified by the prefix of \p
 ///   parameter identifier)
@@ -1034,8 +1034,6 @@ static void find_and_replace_parameter(
 /// Example: class `Outer<T>` has an inner class `Inner` that has a field
 /// `t` of type `Generic<T>`. This function ensures that the parameter points to
 /// `java::Outer::T` instead of `java::Outer$Inner::T`.
-/// \param type
-/// \param replacement_parameters
 static void find_and_replace_parameters(
   typet &type,
   const std::vector<java_generic_parametert> &replacement_parameters)
@@ -1118,8 +1116,6 @@ void convert_java_annotations(
 /// any generic class. All uses of the implicit generic type parameters within
 /// the inner class are updated to point to the type parameters of the
 /// corresponding outer classes.
-/// \param class_name
-/// \param symbol_table
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table)

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -76,11 +76,11 @@ class patternt
 /// 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.
-/// \param[in,out] ftype:
+/// \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:
+/// \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
@@ -191,18 +191,14 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
 /// Returns an expression indicating a local variable suitable to load/store
 /// from a bytecode at address `address` a value of type `type_char` stored in
 /// the JVM's slot `arg`.
-///
-/// \param arg
-///   The local variable slot
-/// \param type_char
-///   The type of the value stored in the slot pointed by `arg`.
-/// \param address
-///   Bytecode address used to find a variable that the LVT declares to be live
-///   and living in the slot pointed by `arg` for this bytecode.
-/// \param do_cast
-///   Indicates whether we should return the original symbol_exprt or a
-///   typecast_exprt if the type of the symbol_exprt does not equal that
-///   represented by `type_char`.
+/// \param arg: The local variable slot
+/// \param type_char: The type of the value stored in the slot pointed by `arg`
+/// \param address: Bytecode address used to find a variable that the LVT
+///   declares to be live and living in the slot pointed by `arg` for this
+///   bytecode
+/// \param do_cast: Indicates whether we should return the original symbol_exprt
+///   or a typecast_exprt if the type of the symbol_exprt does not equal that
+///   represented by `type_char`
 /// \return symbol_exprt or type-cast symbol_exprt
 exprt java_bytecode_convert_methodt::variable(
   const exprt &arg,
@@ -239,18 +235,12 @@ exprt java_bytecode_convert_methodt::variable(
 }
 
 /// Returns the member type for a method, based on signature or descriptor
-/// \param descriptor
-///   descriptor of the method
-/// \param signature
-///   signature of the method
-/// \param class_name
-///   string containing the name of the corresponding class
-/// \param method_name
-///   string containing the name of the method
-/// \param message_handler
-///   message handler to collect warnings
-/// \return
-///   the constructed member type
+/// \param descriptor: descriptor of the method
+/// \param signature: signature of the method
+/// \param class_name: string containing the name of the corresponding class
+/// \param method_name: string containing the name of the method
+/// \param message_handler: message handler to collect warnings
+/// \return the constructed member type
 java_method_typet member_type_lazy(
   const std::string &descriptor,
   const optionalt<std::string> &signature,
@@ -308,9 +298,9 @@ java_method_typet member_type_lazy(
 
 /// Retrieves the symbol of the lambda method associated with the given
 /// lambda method handle (bootstrap method).
-/// \param lambda_method_handles Vector of lambda method handles (bootstrap
+/// \param lambda_method_handles: Vector of lambda method handles (bootstrap
 ///   methods) of the class where the lambda is called
-/// \param index Index of the lambda method handle in the vector
+/// \param index: Index of the lambda method handle in the vector
 /// \return Symbol of the lambda method if the method handle has a known type
 optionalt<symbolt> java_bytecode_convert_methodt::get_lambda_method_symbol(
   const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
@@ -3142,7 +3132,7 @@ irep_idt java_bytecode_convert_methodt::get_static_field(
 /// Create temporary variables if a write instruction can have undesired side-
 /// effects.
 /// \param tmp_var_prefix: The prefix string to use for new temporary variables
-/// \param[out] block: The code block the assignment is added to if required.
+/// \param [out] block: The code block the assignment is added to if required.
 /// \param write_type: The enumeration type of the write instruction.
 /// \param identifier: The identifier of the symbol in the write instruction.
 void java_bytecode_convert_methodt::save_stack_entries(