Skip to content

Commit 1f4a5b0

Browse files
authored
[doc] nit: exec_allows_no_decreases_clause flag (#2617)
1 parent 85faabe commit 1f4a5b0

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

source/docs/guide/src/exec_termination.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,4 @@
22

33
While recursive `spec` functions and `proof` functions must always terminate and therefore must always contain a decreases clause, nontermination is allowed for exec functions. Nevertheless, by default, Verus still requires that recursive `exec` functions and loops in `exec` mode have a `decreases` clause. This only guarantees that the present function will terminate, on the assumption that all the callees also terminate so it should be treated as a lint, not a complete guarantee of termination.
44

5-
The attribute #![verifier::exec_allows_no_decreases_clause] can be used to disable this check for a function, module, or crate.
5+
The attribute [`#![verifier::exec_allows_no_decreases_clause]`](reference-attributes.md#verifierexec_allows_no_decreases_clause) can be used to disable this check for a function, module, or crate.

0 commit comments

Comments
 (0)