Merge pull request #3082 from johnnonweiler/doc/reduce-doxygen-warnings

Reduce doxygen warnings

Author: tautschnig

src/doxyfile

@@ -1020,15 +1020,15 @@ VERBATIM_HEADERS       = YES
 # generated with the -Duse-libclang=ON option for CMake.
 # The default value is: NO.
 
-CLANG_ASSISTED_PARSING = NO
+#CLANG_ASSISTED_PARSING = NO
 
 # If clang assisted parsing is enabled you can provide the compiler with command
 # line options that you would normally use when invoking the compiler. Note that
 # the include paths will already be set by doxygen for the files and directories
 # specified with INPUT and INCLUDE_PATH.
 # This tag requires that the tag CLANG_ASSISTED_PARSING is set to YES.
 
-CLANG_OPTIONS          =
+#CLANG_OPTIONS          =
 
 #---------------------------------------------------------------------------
 # Configuration options related to the alphabetical class index

src/goto-programs/goto_trace.h

@@ -14,13 +14,6 @@ Date: July 2005
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
 
-/*! \file goto-symex/goto_trace.h
- * \brief Traces through goto programs
- *
- * \author Daniel Kroening <[email protected]>
- * \date   Sun Jul 31 21:54:44 BST 2011
-*/
-
 #include <iosfwd>
 #include <vector>
 

src/goto-symex/README.md

@@ -81,7 +81,7 @@ the instruction type, i.e. goto_symext::symex_function_call() if the
 current instruction is a function call, goto_symext::symex_goto() if the
 current instruction is a goto, etc.
 
-\subsection Loop and recursion unwinding
+\subsection symex-loop-and-recursion-unwinding Loop and recursion unwinding
 
 Each backwards goto and recursive call has a separate counter
 (handled by \ref cbmc or another driver program, see the `--unwind` and
@@ -91,7 +91,7 @@ be handled completely (assuming the unwinding limit is sufficient).
 When an unwind or recursion limit is reached, an assertion can be added to
 explicitly show when analysis is incomplete.
 
-\subsection \ref goto_symext::clean_expr
+\subsection goto-symext-clean-expr goto_symext::clean_expr
 
 Before any expression is incorporated into the output equation set it is passed
 through \ref goto_symext::clean_expr and thus \ref goto_symext::dereference,