Skip to content

Commit ccf1e61

Browse files
committed
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.
1 parent 014188e commit ccf1e61

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

doc/architectural/symex-instructions.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,12 @@ Symex is, at its core, a GOTO-program interpreter that uses symbolic values inst
2323
This produces a formula which describes all possible outputs rather than a single output value.
2424
While Symex is interpreting the program, it also builds a list of Static Single Assignment (SSA)
2525
steps that form part of the equation that is to be sent to the solver. For more information see
26-
[src/goto-symex](../../src/goto-symex/README.md).
26+
\ref symbolic-execution.
2727

2828
You can see the main instruction dispatcher (what corresponds to the main interpreter
2929
loop) at `goto_symext::execute_next_instruction`.
3030

31-
Symex's source code is available under [src/goto-symex](../../src/goto-symex/).
31+
Symex's source code is available under \ref goto-symex.
3232

3333
## Instruction Types
3434

@@ -115,7 +115,7 @@ case ASSUME:
115115
break;
116116
```
117117
118-
The way the [`symex` subfolder](../../src/goto-symex/) is structured, the different
118+
The way the \ref goto-symex subfolder is structured, the different
119119
dispatching functions are usually in their own file, designated by the instruction's
120120
name. As an example, you can find the code for the function goto_symext::symex_goto
121121
in [symex_goto.cpp](../../src/goto-symex/symex_goto.cpp)

doc/doxygen-root/doxyfile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -853,6 +853,7 @@ INPUT_ENCODING = UTF-8
853853
FILE_PATTERNS = *.cpp
854854
FILE_PATTERNS += *.h
855855
FILE_PATTERNS += *.md
856+
FILE_PATTERNS += *.c
856857

857858
# The RECURSIVE tag can be used to specify whether or not subdirectories should
858859
# be searched for input files as well.

0 commit comments

Comments
 (0)