diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 91107ffa127..cdabf2adb42 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -638,10 +638,8 @@ bool java_entry_point(
 /// \param message_handler: Where to write output to
 /// \param assume_init_pointers_not_null: When creating pointers, assume they
 ///   always take a non-null value.
-/// \param max_nondet_array_length: The length of the arrays to create when
-///   filling them
-/// \param max_nondet_tree_depth: defines the maximum depth of the object tree
-///   (see java_entry_points documentation for details)
+/// \param assert_uncaught_exceptions: Add an uncaught-exception check
+/// \param object_factory_parameters: Parameters for creation of arguments
 /// \param pointer_type_selector: Logic for substituting types of pointers
 /// \returns true if error occurred on entry point search, false otherwise
 bool generate_java_start_function(
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 0f98c9c2429..2850ac3b1a4 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -176,6 +176,7 @@ class java_object_factoryt
 /// \param allocate_type: type of the object allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
+/// \param function_id: function ID to associate with auxiliary variables
 /// \param output_code: code block to which the necessary code is added
 /// \param symbols_created: created symbols to be declared by the caller
 /// \param cast_needed: Boolean flags saying where we need to cast the malloc
@@ -242,6 +243,7 @@ exprt allocate_dynamic_object(
 ///   allocated
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
+/// \param function_id: function ID to associate with auxiliary variables
 /// \param output_code: code block to which the necessary code is added
 /// \return the dynamic object created
 exprt allocate_dynamic_object_with_decl(
@@ -392,6 +394,8 @@ code_assignt java_object_factoryt::get_null_assignment(
 ///   NO_UPDATE_IN_PLACE: initialize `expr` from scratch
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
 ///   MAY_UPDATE_IN_PLACE: invalid input
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_pointer_target_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -707,6 +711,8 @@ bool initialize_nondet_string_fields(
 ///   * MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
 ///     and MUST_ cases.
 ///   * MUST_UPDATE_IN_PLACE: reinitialize an existing object
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_pointer_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -930,6 +936,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
+/// \param location:
+///   Source location associated with nondet-initialization.
 /// \return
 ///   A symbol expression of type \p replacement_pointer corresponding to a
 ///   pointer to object `tmp_object` (see above).
@@ -994,6 +1002,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
 ///   NO_UPDATE_IN_PLACE: initialize `expr` from scratch
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
 ///   MAY_UPDATE_IN_PLACE: invalid input
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_struct_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -1159,6 +1169,8 @@ void java_object_factoryt::gen_nondet_struct_init(
 ///   MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
 ///   and MUST_ cases.
 ///   MUST_UPDATE_IN_PLACE: reinitialize an existing object
+/// \param location:
+///   Source location associated with nondet-initialization.
 void java_object_factoryt::gen_nondet_init(
   code_blockt &assignments,
   const exprt &expr,
@@ -1307,6 +1319,8 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
 /// \param element_type:
 ///   Actual element type of the array (the array for all reference types will
 ///   have void* type, but this will be annotated as the true member type).
+/// \param location:
+///   Source location associated with nondet-initialization.
 /// \return Appends instructions to `assignments`
 void java_object_factoryt::allocate_nondet_length_array(
   code_blockt &assignments,
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 8ca7b6f2066..5bcda8d23dd 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -695,8 +695,8 @@ inline typet java_type_from_string_with_exception(
 }
 
 /// Get the index in the subtypes array for a given component.
-/// \param t The type we search for the subtypes in.
-/// \param identifier The string identifier of the type of the component.
+/// \param gen_types: The subtypes array.
+/// \param identifier: The string identifier of the type of the component.
 /// \return Optional with the size if the identifier was found.
 inline const optionalt<size_t> java_generics_get_index_for_subtype(
   const std::vector<java_generic_parametert> &gen_types,
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
index 1ac75ce78c4..653790f8de8 100644
--- a/jbmc/src/java_bytecode/replace_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -323,6 +323,9 @@ static void replace_java_nondet(goto_programt &goto_program)
   }
 }
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation in a single function.
+/// \param function: The goto program to modify.
 void replace_java_nondet(goto_model_functiont &function)
 {
   goto_programt &program = function.get_goto_function().body;
@@ -341,6 +344,9 @@ void replace_java_nondet(goto_functionst &goto_functions)
   remove_skip(goto_functions);
 }
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation.
+/// \param goto_model: The goto program to modify.
 void replace_java_nondet(goto_modelt &goto_model)
 {
   replace_java_nondet(goto_model.goto_functions);
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.h b/jbmc/src/java_bytecode/replace_java_nondet.h
index 4a0b00c3b1e..2949d21916f 100644
--- a/jbmc/src/java_bytecode/replace_java_nondet.h
+++ b/jbmc/src/java_bytecode/replace_java_nondet.h
@@ -16,16 +16,10 @@ class goto_modelt;
 class goto_functionst;
 class goto_model_functiont;
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation.
-/// \param goto_model: The goto program to modify.
 void replace_java_nondet(goto_modelt &);
 
 void replace_java_nondet(goto_functionst &);
 
-/// Replace calls to nondet library functions with an internal nondet
-/// representation in a single function.
-/// \param function: The goto program to modify.
 void replace_java_nondet(goto_model_functiont &function);
 
 #endif
diff --git a/src/cbmc/xml_interface.h b/src/cbmc/xml_interface.h
index 945be7624bb..8230d180bad 100644
--- a/src/cbmc/xml_interface.h
+++ b/src/cbmc/xml_interface.h
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/cmdline.h>
 
+class xmlt;
+
 class xml_interfacet
 {
 public:
@@ -24,7 +26,7 @@ class xml_interfacet
 
 protected:
   void get_xml_options(cmdlinet &cmdline);
-  void get_xml_options(const class xmlt &xml, cmdlinet &cmdline);
+  void get_xml_options(const xmlt &xml, cmdlinet &cmdline);
 };
 
 #endif // CPROVER_CBMC_XML_INTERFACE_H
diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h
index abc3b390290..ed4c25f4783 100644
--- a/src/goto-programs/class_hierarchy.h
+++ b/src/goto-programs/class_hierarchy.h
@@ -130,7 +130,6 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
 /// Output the class hierarchy
 /// \param hierarchy: the class hierarchy to be printed
 /// \param message_handler: the message handler
-/// \param ui: the UI format
 /// \param children_only: print the children only and do not print the parents
 void show_class_hierarchy(
   const class_hierarchyt &hierarchy,
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index d4333852dc6..6a83ed46a55 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -260,8 +260,10 @@ bool read_object_and_link(
 }
 
 /// \brief reads an object file, and also updates the config
-/// \param file_name file name of the goto binary
-/// \param message_handler for diagnostics
+/// \param file_name: file name of the goto binary
+/// \param dest_symbol_table: symbol table to update
+/// \param dest_functions: collection of goto functions to update
+/// \param message_handler: for diagnostics
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 5671e7ed281..65c805a8b65 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -27,14 +27,12 @@ void optionst::set_option(const std::string &option,
   set_option(option, std::string(value?"1":"0"));
 }
 
-void optionst::set_option(const std::string &option,
-                          const signed int value)
+void optionst::set_option(const std::string &option, const int value)
 {
   set_option(option, std::to_string(value));
 }
 
-void optionst::set_option(const std::string &option,
-                          const unsigned int value)
+void optionst::set_option(const std::string &option, const unsigned value)
 {
   set_option(option, std::to_string(value));
 }
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 8317d68fe32..bf7e5cc245e 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -79,7 +79,7 @@ class symbol_typet:public typet
 
 /// Check whether a reference to a typet is a \ref symbol_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref symbol_typet.
+/// \return True if \p type is a \ref symbol_typet.
 template <>
 inline bool can_cast_type<symbol_typet>(const typet &type)
 {
@@ -243,7 +243,7 @@ class struct_union_typet:public typet
 
 /// Check whether a reference to a typet is a \ref struct_union_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref struct_union_typet.
+/// \return True if \p type is a \ref struct_union_typet.
 template <>
 inline bool can_cast_type<struct_union_typet>(const typet &type)
 {
@@ -351,7 +351,7 @@ class struct_typet:public struct_union_typet
 
 /// Check whether a reference to a typet is a \ref struct_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref struct_typet.
+/// \return True if \p type is a \ref struct_typet.
 template <>
 inline bool can_cast_type<struct_typet>(const typet &type)
 {
@@ -411,7 +411,7 @@ class class_typet:public struct_typet
 
 /// Check whether a reference to a typet is a \ref class_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref class_typet.
+/// \return True if \p type is a \ref class_typet.
 template <>
 inline bool can_cast_type<class_typet>(const typet &type)
 {
@@ -452,7 +452,7 @@ class union_typet:public struct_union_typet
 
 /// Check whether a reference to a typet is a \ref union_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref union_typet.
+/// \return True if \p type is a \ref union_typet.
 template <>
 inline bool can_cast_type<union_typet>(const typet &type)
 {
@@ -504,7 +504,7 @@ class tag_typet:public typet
 
 /// Check whether a reference to a typet is a \ref tag_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref tag_typet.
+/// \return True if \p type is a \ref tag_typet.
 template <>
 inline bool can_cast_type<tag_typet>(const typet &type)
 {
@@ -545,7 +545,7 @@ class struct_tag_typet:public tag_typet
 
 /// Check whether a reference to a typet is a \ref struct_tag_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref struct_tag_typet.
+/// \return True if \p type is a \ref struct_tag_typet.
 template <>
 inline bool can_cast_type<struct_tag_typet>(const typet &type)
 {
@@ -585,7 +585,7 @@ class union_tag_typet:public tag_typet
 
 /// Check whether a reference to a typet is a \ref union_tag_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref union_tag_typet.
+/// \return True if \p type is a \ref union_tag_typet.
 template <>
 inline bool can_cast_type<union_tag_typet>(const typet &type)
 {
@@ -635,7 +635,7 @@ class enumeration_typet:public typet
 
 /// Check whether a reference to a typet is a \ref enumeration_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref enumeration_typet.
+/// \return True if \p type is a \ref enumeration_typet.
 template <>
 inline bool can_cast_type<enumeration_typet>(const typet &type)
 {
@@ -699,7 +699,7 @@ class c_enum_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref c_enum_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref c_enum_typet.
+/// \return True if \p type is a \ref c_enum_typet.
 template <>
 inline bool can_cast_type<c_enum_typet>(const typet &type)
 {
@@ -739,7 +739,7 @@ class c_enum_tag_typet:public tag_typet
 
 /// Check whether a reference to a typet is a \ref c_enum_tag_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref c_enum_tag_typet.
+/// \return True if \p type is a \ref c_enum_tag_typet.
 template <>
 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
 {
@@ -984,7 +984,7 @@ class code_typet:public typet
 
 /// Check whether a reference to a typet is a \ref code_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref code_typet.
+/// \return True if \p type is a \ref code_typet.
 template <>
 inline bool can_cast_type<code_typet>(const typet &type)
 {
@@ -1050,7 +1050,7 @@ class array_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref array_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref array_typet.
+/// \return True if \p type is a \ref array_typet.
 template <>
 inline bool can_cast_type<array_typet>(const typet &type)
 {
@@ -1089,7 +1089,7 @@ class incomplete_array_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref incomplete_array_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref incomplete_array_typet.
+/// \return True if \p type is a \ref incomplete_array_typet.
 template <>
 inline bool can_cast_type<incomplete_array_typet>(const typet &type)
 {
@@ -1162,7 +1162,7 @@ class bitvector_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref bitvector_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref bitvector_typet.
+/// \return True if \p type is a \ref bitvector_typet.
 template <>
 inline bool can_cast_type<bitvector_typet>(const typet &type)
 {
@@ -1209,7 +1209,7 @@ class bv_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref bv_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref bv_typet.
+/// \return True if \p type is a \ref bv_typet.
 template <>
 inline bool can_cast_type<bv_typet>(const typet &type)
 {
@@ -1264,7 +1264,7 @@ class unsignedbv_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref unsignedbv_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref unsignedbv_typet.
+/// \return True if \p type is a \ref unsignedbv_typet.
 template <>
 inline bool can_cast_type<unsignedbv_typet>(const typet &type)
 {
@@ -1320,7 +1320,7 @@ class signedbv_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref signedbv_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref signedbv_typet.
+/// \return True if \p type is a \ref signedbv_typet.
 template <>
 inline bool can_cast_type<signedbv_typet>(const typet &type)
 {
@@ -1384,7 +1384,7 @@ class fixedbv_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref fixedbv_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref fixedbv_typet.
+/// \return True if \p type is a \ref fixedbv_typet.
 template <>
 inline bool can_cast_type<fixedbv_typet>(const typet &type)
 {
@@ -1446,7 +1446,7 @@ class floatbv_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref floatbv_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref floatbv_typet.
+/// \return True if \p type is a \ref floatbv_typet.
 template <>
 inline bool can_cast_type<floatbv_typet>(const typet &type)
 {
@@ -1498,7 +1498,7 @@ class c_bit_field_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref c_bit_field_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref c_bit_field_typet.
+/// \return True if \p type is a \ref c_bit_field_typet.
 template <>
 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
 {
@@ -1543,7 +1543,7 @@ class pointer_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref pointer_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref pointer_typet.
+/// \return True if \p type is a \ref pointer_typet.
 template <>
 inline bool can_cast_type<pointer_typet>(const typet &type)
 {
@@ -1596,7 +1596,7 @@ class reference_typet:public pointer_typet
 
 /// Check whether a reference to a typet is a \ref reference_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref reference_typet.
+/// \return True if \p type is a \ref reference_typet.
 template <>
 inline bool can_cast_type<reference_typet>(const typet &type)
 {
@@ -1645,7 +1645,7 @@ class c_bool_typet:public bitvector_typet
 
 /// Check whether a reference to a typet is a \ref c_bool_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref c_bool_typet.
+/// \return True if \p type is a \ref c_bool_typet.
 template <>
 inline bool can_cast_type<c_bool_typet>(const typet &type)
 {
@@ -1695,7 +1695,7 @@ class string_typet:public typet
 
 /// Check whether a reference to a typet is a \ref string_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref string_typet.
+/// \return True if \p type is a \ref string_typet.
 template <>
 inline bool can_cast_type<string_typet>(const typet &type)
 {
@@ -1742,7 +1742,7 @@ class range_typet:public typet
 
 /// Check whether a reference to a typet is a \ref range_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref range_typet.
+/// \return True if \p type is a \ref range_typet.
 template <>
 inline bool can_cast_type<range_typet>(const typet &type)
 {
@@ -1801,7 +1801,7 @@ class vector_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref vector_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref vector_typet.
+/// \return True if \p type is a \ref vector_typet.
 template <>
 inline bool can_cast_type<vector_typet>(const typet &type)
 {
@@ -1845,7 +1845,7 @@ class complex_typet:public type_with_subtypet
 
 /// Check whether a reference to a typet is a \ref complex_typet.
 /// \param type Source type.
-/// \return True if \param type is a \ref complex_typet.
+/// \return True if \p type is a \ref complex_typet.
 template <>
 inline bool can_cast_type<complex_typet>(const typet &type)
 {