From 69f4f3bf7afd0d862df99c71f6f6ff4ead9111f0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 13 Jan 2025 14:35:58 +0000
Subject: [PATCH] Address Doxygen warnings

Doxygen 1.9.8 detects more problems than earlier versions did.
---
 doc/API/util/piped_process.md                     | 5 +++--
 doc/architectural/front-page.md                   | 4 ++--
 doc/architectural/goto-program-transformations.md | 2 +-
 doc/assets/xml_spec.md                            | 2 +-
 src/goto-instrument/README.md                     | 6 +++---
 5 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/doc/API/util/piped_process.md b/doc/API/util/piped_process.md
index f0b1854f860..f01007b1d97 100644
--- a/doc/API/util/piped_process.md
+++ b/doc/API/util/piped_process.md
@@ -1,6 +1,7 @@
-\page piped-process `src/util/piped_process.{cpp, h}`
+\page piped-process The `piped_process` API
 
-To utilise the `piped_process` API for interprocess communication with any binary:
+To utilise the `piped_process` API (`src/util/piped_process.{cpp, h}`) for
+interprocess communication with any binary:
 
 * You need to initialise it by calling the construct `piped_processt("binary with args")`.
   * If IPC fails before child process creation, you will get a `system_exceptiont`.
diff --git a/doc/architectural/front-page.md b/doc/architectural/front-page.md
index 1c08c024854..a729da7b769 100644
--- a/doc/architectural/front-page.md
+++ b/doc/architectural/front-page.md
@@ -54,7 +54,7 @@ license</a>.
 Overview of Documentation
 =======
 
-### For users:
+## For users:
 
 * The [CPROVER User Manual](http://www.cprover.org/cprover-manual/) details the
   capabilities of CBMC and describes how to install and use these tools. It
@@ -68,7 +68,7 @@ you can access it <a href=
 * \subpage memory-bounds-checking
 * \subpage satabs
 
-### For contributors:
+## For contributors:
 
 The following pages attempt to provide the information that a developer needs to
 work on CBMC, in a sensible order. In many cases they link to the appropriate
diff --git a/doc/architectural/goto-program-transformations.md b/doc/architectural/goto-program-transformations.md
index 8415b8333a1..1e68c8645b8 100644
--- a/doc/architectural/goto-program-transformations.md
+++ b/doc/architectural/goto-program-transformations.md
@@ -176,7 +176,7 @@ This pass adds failed symbols to the symbol table. See
 `src/pointer-analysis/add_failed_symbols.h` for details. The implementation of
 this pass is called via \ref add_failed_symbols(symbol_table_baset &) . The
 purpose of failed symbols is explained in the documentation of the function \ref
-goto_symext::dereference(exprt &, statet &, bool)
+goto_symext::dereference(exprt &, goto_symex_statet &, bool)
 
 <em>Predecessor pass is \ref update-transform or the optional \ref
 nondet-transform if it is being used.</em>
diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md
index b5591cc4203..8a6da1f71b2 100644
--- a/doc/assets/xml_spec.md
+++ b/doc/assets/xml_spec.md
@@ -475,7 +475,7 @@ The path from the input C code to XML trace goes through the following
 steps:\
 `C` → `GOTO` → `SSA` → `GOTO Trace` → `XML Trace`
 
-#### SSA to GOTO Trace
+### SSA to GOTO Trace
 
 SSA steps are sorted by clocks and the following steps are skipped: PHI,
 GUARD assignments; shared-read, shared-write, constraint, spawn,
diff --git a/src/goto-instrument/README.md b/src/goto-instrument/README.md
index e2fcf92734c..a925dd4a335 100644
--- a/src/goto-instrument/README.md
+++ b/src/goto-instrument/README.md
@@ -27,7 +27,7 @@ from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
 skeleton of their application. The `doit()` method in `parseoptions.cpp`
 is the preferred location for the top level control for the program.
 
-### Main usage ###
+## Main usage ##
 
 For most of the transformations, `goto-instrument` takes one or two 
 arguments and any number of options. The two file arguments are 
@@ -40,7 +40,7 @@ option output, with no indication of what has gone wrong. Some of the options
 can work with just an input file and not output file. For more specific
 examples, take a look at the demonstrations below:
 
-### Function pointer removal ###
+## Function pointer removal ##
 
 As an example of a transformation pass being run, imagine you have a file 
 called `function_pointers.c` with the following content:
@@ -163,7 +163,7 @@ You can now see that the function pointer (indirect) call (resulting from
 the array indexing of the array containing the function pointers) 
 has now been substituted by direct, conditional calls.
 
-### Call Graph ###
+## Call Graph ##
 
 This is an example of a command line flag that requires only one argument,
 specifying the input file.