File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -81,7 +81,7 @@ the instruction type, i.e. goto_symext::symex_function_call() if the
81
81
current instruction is a function call, goto_symext::symex_goto() if the
82
82
current instruction is a goto, etc.
83
83
84
- \subsection Loop and recursion unwinding
84
+ \subsection symex-loop-and-recursion-unwinding Loop and recursion unwinding
85
85
86
86
Each backwards goto and recursive call has a separate counter
87
87
(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).
91
91
When an unwind or recursion limit is reached, an assertion can be added to
92
92
explicitly show when analysis is incomplete.
93
93
94
- \subsection \ref goto_symext::clean_expr
94
+ \subsection goto-symext-clean-expr goto_symext::clean_expr
95
95
96
96
Before any expression is incorporated into the output equation set it is passed
97
97
through \ref goto_symext::clean_expr and thus \ref goto_symext::dereference,
You can’t perform that action at this time.
0 commit comments