diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
index e0f230384f9..b4ae9886c7a 100644
--- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp
+++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -35,7 +35,7 @@ codet character_refine_preprocesst::convert_char_function(
 
 /// The returned expression is true when the first argument is in the interval
 /// defined by the lower and upper bounds (included)
-/// \param arg: Expression we want to bound
+/// \param chr: Expression we want to bound
 /// \param lower_bound: Integer lower bound
 /// \param upper_bound: Integer upper bound
 /// \return A Boolean expression
@@ -65,7 +65,7 @@ exprt character_refine_preprocesst::in_list_expr(
 
 /// Determines the number of char values needed to represent the specified
 /// character (Unicode code point).
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A integer expression of the given type
 exprt character_refine_preprocesst::expr_of_char_count(
@@ -308,7 +308,7 @@ codet character_refine_preprocesst::convert_hash_code(conversion_inputt &target)
 /// Returns the leading surrogate (a high surrogate code unit) of the surrogate
 /// pair representing the specified supplementary character (Unicode code point)
 /// in the UTF-16 encoding.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return An expression of the given type
 exprt character_refine_preprocesst::expr_of_high_surrogate(
@@ -342,7 +342,7 @@ exprt character_refine_preprocesst::expr_of_is_ascii_lower_case(
 }
 
 /// Determines if the specified character is an ASCII uppercase character.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_ascii_upper_case(
@@ -356,7 +356,7 @@ exprt character_refine_preprocesst::expr_of_is_ascii_upper_case(
 ///    TODO: for now this is only for ASCII characters, the
 ///          following unicode categories are not yet considered:
 ///          TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return An expression of the given type
 exprt character_refine_preprocesst::expr_of_is_letter(
@@ -374,7 +374,7 @@ exprt character_refine_preprocesst::expr_of_is_letter(
 ///          TITLECASE_LETTER MODIFIER_LETTER OTHER_LETTER LETTER_NUMBER
 ///          and contributory property Other_Alphabetic as defined by the
 ///          Unicode Standard.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return An expression of the given type
 exprt character_refine_preprocesst::expr_of_is_alphabetic(
@@ -396,7 +396,7 @@ codet character_refine_preprocesst::convert_is_alphabetic(
 /// Determines whether the specified character (Unicode code point) is in the
 /// Basic Multilingual Plane (BMP). Such code points can be represented using a
 /// single char.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_bmp_code_point(
@@ -417,7 +417,7 @@ codet character_refine_preprocesst::convert_is_bmp_code_point(
 }
 
 /// Determines if a character is defined in Unicode.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return An expression of the given type
 exprt character_refine_preprocesst::expr_of_is_defined(
@@ -475,11 +475,11 @@ codet character_refine_preprocesst::convert_is_defined_int(
 /// DECIMAL_DIGIT_NUMBER.
 ///
 ///   TODO: for now we only support these ranges of digits:
-///         '\u0030' through '\u0039', ISO-LATIN-1 digits ('0' through '9')
-///         '\u0660' through '\u0669', Arabic-Indic digits
-///         '\u06F0' through '\u06F9', Extended Arabic-Indic digits
-///         '\u0966' through '\u096F', Devanagari digits
-///         '\uFF10' through '\uFF19', Fullwidth digits
+///         '\\u0030' through '\\u0039', ISO-LATIN-1 digits ('0' through '9')
+///         '\\u0660' through '\\u0669', Arabic-Indic digits
+///         '\\u06F0' through '\\u06F9', Extended Arabic-Indic digits
+///         '\\u0966' through '\\u096F', Devanagari digits
+///         '\\uFF10' through '\\uFF19', Fullwidth digits
 ///         Many other character ranges contain digits as well.
 /// \param chr: An expression of type character
 /// \param type: A type for the output
@@ -519,7 +519,7 @@ codet character_refine_preprocesst::convert_is_digit_int(
 
 /// Determines if the given char value is a Unicode high-surrogate code unit
 /// (also known as leading-surrogate code unit).
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_high_surrogate(
@@ -539,11 +539,11 @@ codet character_refine_preprocesst::convert_is_high_surrogate(
 }
 
 /// Determines if the character is one of ignorable in a Java identifier, that
-/// is, it is in one of these ranges: '\u0000' through '\u0008' '\u000E' through
-/// '\u001B' '\u007F' through '\u009F'
+/// is, it is in one of these ranges: '\\u0000' through '\\u0008' '\\u000E'
+/// through '\\u001B' '\\u007F' through '\\u009F'
 ///
 ///    TODO: For now, we ignore the FORMAT general category value
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_identifier_ignorable(
@@ -770,7 +770,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate(
 /// specification.
 ///
 ///    TODO: For now only ASCII characters are considered
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return An expression of the given type
 exprt character_refine_preprocesst::expr_of_is_mirrored(
@@ -812,7 +812,7 @@ codet character_refine_preprocesst::convert_is_space(conversion_inputt &target)
 
 /// Determines if the specified character is white space according to Unicode
 /// (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR)
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_space_char(
@@ -846,7 +846,7 @@ codet character_refine_preprocesst::convert_is_space_char_int(
 
 /// Determines whether the specified character (Unicode code point) is in the
 /// supplementary character range.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_supplementary_code_point(
@@ -866,7 +866,7 @@ codet character_refine_preprocesst::convert_is_supplementary_code_point(
 }
 
 /// Determines if the given char value is a Unicode surrogate code unit.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_surrogate(
@@ -902,7 +902,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair(
 }
 
 /// Determines if the specified character is a titlecase character.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_title_case(
@@ -939,7 +939,7 @@ codet character_refine_preprocesst::convert_is_title_case_int(
 
 /// Determines if the specified character is in the LETTER_NUMBER category of
 /// Unicode
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_letter_number(
@@ -966,7 +966,7 @@ exprt character_refine_preprocesst::expr_of_is_letter_number(
 ///
 ///    TODO: For now we do not allow connecting punctuation, combining mark,
 ///          non-spacing mark
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_unicode_identifier_part(
@@ -1074,9 +1074,9 @@ codet character_refine_preprocesst::convert_is_valid_code_point(
 /// Determines if the specified character is white space according to Java. It
 /// is the case when it one of the following: * a Unicode space character
 /// (SPACE_SEPARATOR, LINE_SEPARATOR, or PARAGRAPH_SEPARATOR) but is not also a
-/// non-breaking space ('\u00A0', '\u2007', '\u202F'). * it is one of these:
+/// non-breaking space ('\\u00A0', '\\u2007', '\\u202F'). * it is one of these:
 /// U+0009  U+000A U+000B U+000C U+000D U+001C U+001D U+001E U+001F
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A Boolean expression
 exprt character_refine_preprocesst::expr_of_is_whitespace(
@@ -1115,7 +1115,7 @@ codet character_refine_preprocesst::convert_is_whitespace_int(
 /// Returns the trailing surrogate (a low surrogate code unit) of the surrogate
 /// pair representing the specified supplementary character (Unicode code point)
 /// in the UTF-16 encoding.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A integer expression of the given type
 exprt character_refine_preprocesst::expr_of_low_surrogate(
@@ -1138,7 +1138,7 @@ codet character_refine_preprocesst::convert_low_surrogate(
 
 /// Returns the value obtained by reversing the order of the bytes in the
 /// specified char value.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A character expression of the given type
 exprt character_refine_preprocesst::expr_of_reverse_bytes(
@@ -1164,7 +1164,7 @@ codet character_refine_preprocesst::convert_reverse_bytes(
 /// (Basic Multilingual Plane or Plane 0) value, the resulting char array has
 /// the same value as codePoint. If the specified code point is a supplementary
 /// code point, the resulting char array has the corresponding surrogate pair.
-/// \param expr: An expression of type character
+/// \param chr: An expression of type character
 /// \param type: A type for the output
 /// \return A character array expression of the given type
 exprt character_refine_preprocesst::expr_of_to_chars(
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 01a082c217e..3c39562e477 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -1074,7 +1074,7 @@ static void find_and_replace_parameters(
 
 /// Convert parsed annotations into the symbol table
 /// \param parsed_annotations: The parsed annotations to convert
-/// \param annotations: The java_annotationt collection to populate
+/// \param java_annotations: The java_annotationt collection to populate
 void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
   std::vector<java_annotationt> &java_annotations)
diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp
index 213bdecabc2..4b864adbb10 100644
--- a/src/analyses/local_safe_pointers.cpp
+++ b/src/analyses/local_safe_pointers.cpp
@@ -177,7 +177,6 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
-/// \param ns: global namespace
 void local_safe_pointerst::output(
   std::ostream &out, const goto_programt &goto_program)
 {
@@ -219,7 +218,6 @@ void local_safe_pointerst::output(
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
-/// \param ns: global namespace
 void local_safe_pointerst::output_safe_dereferences(
   std::ostream &out, const goto_programt &goto_program)
 {
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 9ced322139a..bd9e179ea42 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -1517,7 +1517,7 @@ void instrumentert::print_outputs(memory_modelt model, bool hide_internals)
   table.close();
 }
 
-/// Note: can be distributed (#define DISTRIBUTED)
+/// Note: can be distributed (\#define DISTRIBUTED)
 #if 1
 // #ifdef _WIN32
 void instrumentert::collect_cycles_by_SCCs(memory_modelt model)
diff --git a/src/solvers/README.md b/src/solvers/README.md
index a9a9a3639c9..ce1487e9682 100644
--- a/src/solvers/README.md
+++ b/src/solvers/README.md
@@ -308,7 +308,7 @@ allocates a new string before calling a primitive.
     \copybrief add_axioms_for_parse_int
     \link add_axioms_for_parse_int More... \endlink
 
-\subsection deprecated Deprecated primitives:
+\subsection solvers-deprecated Deprecated primitives:
 
   * `cprover_string_concat_code_point`, `cprover_string_code_point_at`,
     `cprover_string_code_point_before`, `cprover_string_code_point_count`:
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index f92bce2211d..2786f91e0e8 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -104,8 +104,6 @@ class string_constraintt final
 };
 
 /// Used for debug printing.
-/// \param [in] ns: namespace for `from_expr`
-/// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
 inline std::string to_string(const string_constraintt &expr)
@@ -176,8 +174,6 @@ class string_not_contains_constraintt : public exprt
 };
 
 /// Used for debug printing.
-/// \param [in] ns: namespace for `from_expr`
-/// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
 inline std::string to_string(const string_not_contains_constraintt &expr)
diff --git a/src/util/README.md b/src/util/README.md
index 1b444ca5643..89b4850e4b7 100644
--- a/src/util/README.md
+++ b/src/util/README.md
@@ -89,8 +89,8 @@ efficient to store many copies of the same string. The static list of strings
 is initially populated from `irep_ids.def`, so for example the fourth entry
 in `irep_ids.def` is `“IREP_ID_ONE(type)”`, so the string “type” has index 3.
 You can refer to this \ref irep_idt as `ID_type`. The other kind of line you
-see is `“IREP_ID_TWO(C_source_location, #source_location)”`, which means the
-\ref irep_idt for the string “#source_location” can be referred to as
+see is \c "IREP_ID_TWO(C_source_location, #source_location)", which means the
+\ref irep_idt for the string “\#source_location” can be referred to as
 `ID_C_source_location`. The “C” is for comment, meaning that it should be
 stored in the [comments](\ref irept::dt::comments). Any strings that need
 to be stored as [irep_idt](\ref irep_idt)s which aren't in `irep_ids.def`
diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h
index 132a1784d7b..05c63b24481 100644
--- a/src/util/expr_iterator.h
+++ b/src/util/expr_iterator.h
@@ -19,7 +19,8 @@
 
 // Forward declarations - table of contents
 
-/// \file Forward depth-first search iterators
+/// \file
+/// Forward depth-first search iterators
 /// These iterators' copy operations are expensive, so use auto&, and avoid
 /// std::next(), std::prev() and post-increment iterator
 ///
diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h
index 7d946bed305..b96ff929f25 100644
--- a/src/util/irep_ids.h
+++ b/src/util/irep_ids.h
@@ -22,7 +22,8 @@ Author: Reuben Thomas, reuben.thomas@me.com
 #include <string>
 #endif
 
-/// \file The irep_ids are generated using a technique called
+/// \file
+/// The irep_ids are generated using a technique called
 /// [X-macros](https://en.wikipedia.org/wiki/X_Macro).
 /// The ids are defined in the file irep_ids.def, using a pair of macros
 /// `IREP_ID_ONE` and `IREP_ID_TWO`.