Add \ref in lots of places

It often doesn't work when backticks are used, so I've removed them.
They don't affect how the text appears that much when I look at the
html.

Author: Owen Jones

src/util/dstring.h

@@ -16,15 +16,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "string_container.h"
 
-/// `dstringt` has one field, an unsigned integer `no` which is an index into
+/// \ref dstringt has one field, an unsigned integer \ref no which is an index into
 /// a static table of strings. This makes it expensive to create a new string
 /// (because you have to look through the whole table to see if it is already
 /// there, and add it if it isn't) but very cheap to compare strings (just
 /// compare the two integers). It also means that when you have lots of copies
 /// of the same string you only have to store the whole string once, which
 /// saves space.
 ///
-/// `irep_idt` and `irep_namet` are typedef-ed to `dstringt` in irep.h unless
+/// `irep_idt` and `irep_namet` are typedef-ed to \ref dstringt in irep.h unless
 /// `USE_STD_STRING` is set.
 ///
 ///

src/util/irep.h

@@ -85,72 +85,72 @@ const irept &get_nil_irep();
 /// \brief Base class for tree-like data structures with sharing
 ///
 /// There are a large number of kinds of tree structured or tree-like data in
-/// CPROVER. `irept` provides a single, unified representation for all of
+/// CPROVER. \ref irept provides a single, unified representation for all of
 /// these, allowing structure sharing and reference counting of data. As
-/// such `irept` is the basic unit of data in CPROVER.  Each `irept`
+/// such \ref irept is the basic unit of data in CPROVER.  Each \ref irept
 /// contains (or references, if reference counted data sharing is enabled, as
 /// it is by default - see the `SHARING` macro) a basic unit of data (of type
-/// `dt`) which contains four things:
+/// \ref dt) which contains four things:
 ///
-/// * `data`:   A string, which is returned when the `id()` function is used.
-///   (Unless `USE_STD_STRING` is set, this is actually a `dstring` and thus
+/// * \ref irept::dt::data : A string, which is returned when the \ref id() function is used.
+///   (Unless `USE_STD_STRING` is set, this is actually a \ref dstringt and thus
 ///   an integer which is a reference into a string table.)
 ///
-/// * `named_sub`:   A map from `irep_namet` (a string) to `irept`. This
+/// * \ref irept::dt::named_sub : A map from `irep_namet` (a string) to \ref irept. This
 ///   is used for named children, i.e.  subexpressions, parameters, etc.
 ///
-/// * `comments`:   Another map from `irep_namet` to `irept` which is used
+/// * \ref irept::dt::comments : Another map from `irep_namet` to \ref irept which is used
 ///   for annotations and other ‘non-semantic’ information. Note that this
-///   map is ignore by the default `operator==`.
+///   map is ignore by the default \ref operator==.
 ///
-/// * `sub`:   A vector of `irept` which is used to store ordered but
+/// * \ref irept::dt::sub : A vector of \ref irept which is used to store ordered but
 ///   unnamed children.
 ///
-/// The `irept::pretty` function outputs the explicit tree structure of
-/// an `irept` and can be used to understand and debug problems with
+/// The \ref irept::pretty function outputs the explicit tree structure of
+/// an \ref irept and can be used to understand and debug problems with
 /// `irept`s.
 ///
 /// On their own `irept`s do not "mean" anything; they are effectively
 /// generic tree nodes. Their interpretation depends on the contents of
-/// result of the `id` function (the `data`) field. `util/irep_ids.def`
+/// result of the \ref id() function, i.e. the `data` field. `util/irep_ids.def`
 /// contains a list of `id` values. During the build process it is used
 /// to generate `util/irep_ids.h` which gives constants for each id
 /// (named `ID_`). You can also make `irep_id`s which do not come from
-/// `util/irep_ids.def`. An `irep_id`can then be used to identify what
-/// kind of data `irept` stores and thus what can be done with it.
+/// `util/irep_ids.def`. An `irep_idt` can then be used to identify what
+/// kind of data the \ref irept stores and thus what can be done with it.
 ///
 /// To simplify this process, there are a variety of classes that inherit
-/// from `irept`, roughly corresponding to the ids listed (i.e.  `ID_or`
-/// (the string `"or”`) corresponds to the class `or_exprt`). These give
+/// from \ref irept, roughly corresponding to the ids listed (i.e. `ID_or`
+/// (the string "or”) corresponds to the class \ref or_exprt). These give
 /// semantically relevant accessor functions for the data; effectively
 /// different APIs for the same underlying data structure. None of these
 /// classes add fields (only methods) and so static casting can be used. The
-/// inheritance graph of the subclasses of `irept` is a useful starting
+/// inheritance graph of the subclasses of \ref irept is a useful starting
 /// point for working out how to manipulate data.
 ///
 /// There are three main groups of classes (or APIs); those derived from
-/// `typet`, `codet` and `exprt` respectively. Although all of these inherit
-/// from `irept`, these are the most abstract level that code should handle
+/// \ref typet, \ref codet and \ref exprt respectively. Although all of these inherit
+/// from \ref irept, these are the most abstract level that code should handle
 /// data. If code is manipulating plain `irept`s then something is wrong
 /// with the architecture of the code.
 ///
-/// Many of the key descendant of `exprt` are declared in `std_expr.h`. All
-/// expressions have a named subexpresion with ID `type`, which gives the
+/// Many of the key descendants of \ref exprt are declared in \ref std_expr.h. All
+/// expressions have a named subexpression with ID "type", which gives the
 /// type of the expression (slightly simplified from C/C++ as
-/// `unsignedbv_typet`, `signedbv_typet`, `floatbv_typet`, etc.). All type
+/// \ref unsignedbv_typet, \ref signedbv_typet, \ref floatbv_typet, etc.). All type
 /// conversions are explicit with an expression with `id() == ID_typecast`
-/// and a `typecast_exprt`. One key descendant of `exprt` is `symbol_exprt`
-/// which creates `irept` instances with the id of “symbol”. These are used
+/// and a \ref typecast_exprt. One key descendant of \ref exprt is \ref symbol_exprt
+/// which creates \ref irept instances with ID “symbol”. These are used
 /// to represent variables; the name of which can be found using the
 /// `get_identifier` accessor function.
 ///
-/// `codet` inherits from `exprt` and is defined in `std_code.h`. It
+/// \ref codet inherits from \ref exprt and is defined in `std_code.h`. It
 /// represents executable code; statements in a C-like language rather than
 /// expressions. In the front-end there are versions of these that hold
 /// whole code blocks, but in goto-programs these have been flattened so
-/// that each `irept` represents one sequence point (almost one line of
-/// code / one semi-colon). The most common descendant of `codet` is
-/// `code_assignt` so a common pattern is to cast the `codet` to an
+/// that each \ref irept represents one sequence point (almost one line of
+/// code / one semi-colon). The most common descendant of \ref codet is
+/// \ref code_assignt so a common pattern is to cast the \ref codet to an
 /// assignment and then recurse on the expression on either side.
 class irept
 {