diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index c7b33c52491..039c622067f 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -29,7 +29,7 @@ Each of these translation passes is implemented in a specific class: @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh @ref dfcc_pointer_in_ranget | Implements @ref contracts-dev-spec-pointer-in-range - @ref dfcc_pointer_euqalst | Implements @ref contracts-dev-spec-pointer-equals + @ref dfcc_pointer_equalst | Implements @ref contracts-dev-spec-pointer-equals @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract