Fix documentation links

1) Make sure .c source files are considered by Doxygen. (Notably,
cprover_contracts.c contains relevant documentation.)
2) Reference other files in ways understood by Doxygen.

Author: tautschnig

doc/architectural/cbmc-architecture.md

@@ -61,7 +61,7 @@ transformation tools (see \ref other-tools).
 
 For an explanation of the data structures involved in the modeling of a GOTO
 program (the GOTO Intermediate Representation used by CBMC and assorted tools)
-please see \subpage central-data-structures .
+please see [central data structures](central-data-structures.md).
 
 ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing
 

doc/architectural/symex-instructions.md

@@ -23,7 +23,7 @@ Symex is, at its core, a GOTO-program interpreter that uses symbolic values inst
 This produces a formula which describes all possible outputs rather than a single output value.
 While Symex is interpreting the program, it also builds a list of Static Single Assignment (SSA)
 steps that form part of the equation that is to be sent to the solver. For more information see
-[src/goto-symex](../../src/goto-symex/README.md).
+[src/goto-symex](../../src/goto-symex/).
 
 You can see the main instruction dispatcher (what corresponds to the main interpreter
 loop) at `goto_symext::execute_next_instruction`.
@@ -128,4 +128,4 @@ potential paths within it.
 
 This is a high-level overview of symex and goto-program instructions.
 For more information (and a more robust introduction), please have a look
-at \ref symbolic-execution.
+at [symbolic-execution](../../src/goto-symex/).

doc/doxygen-root/doxyfile

@@ -853,6 +853,7 @@ INPUT_ENCODING         = UTF-8
 FILE_PATTERNS          = *.cpp
 FILE_PATTERNS         += *.h
 FILE_PATTERNS         += *.md
+FILE_PATTERNS         += *.c
 
 # The RECURSIVE tag can be used to specify whether or not subdirectories should
 # be searched for input files as well.