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.