From ccf1e619481355c6a4a45caa77153169e23ca717 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 6 Mar 2023 15:10:40 +0000 Subject: [PATCH] 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. --- doc/architectural/symex-instructions.md | 6 +++--- doc/doxygen-root/doxyfile | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/architectural/symex-instructions.md b/doc/architectural/symex-instructions.md index 326802f1265..d2c82bab173 100644 --- a/doc/architectural/symex-instructions.md +++ b/doc/architectural/symex-instructions.md @@ -23,12 +23,12 @@ 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). +\ref symbolic-execution. You can see the main instruction dispatcher (what corresponds to the main interpreter loop) at `goto_symext::execute_next_instruction`. -Symex's source code is available under [src/goto-symex](../../src/goto-symex/). +Symex's source code is available under \ref goto-symex. ## Instruction Types @@ -115,7 +115,7 @@ case ASSUME: break; ``` -The way the [`symex` subfolder](../../src/goto-symex/) is structured, the different +The way the \ref goto-symex subfolder is structured, the different dispatching functions are usually in their own file, designated by the instruction's name. As an example, you can find the code for the function goto_symext::symex_goto in [symex_goto.cpp](../../src/goto-symex/symex_goto.cpp) diff --git a/doc/doxygen-root/doxyfile b/doc/doxygen-root/doxyfile index 2c02f89dd60..19a4f2d8574 100644 --- a/doc/doxygen-root/doxyfile +++ b/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.